2014-06-15から1日間の記事一覧
http://d.hatena.ne.jp/ehito/20130816/1376622603 の続編です. 前回は n≦n*n を sub goal としましたが,今回は結論に含め,帰納法の仮定を強くしました. g `!n. &0 <= &n * (&n - &1) * (&n - &2) /\ &0 <= &n * (&n - &1) /\ &1 + &n + &n * (&n - &1) …
http://d.hatena.ne.jp/ehito/20130816/1376622603 の続編です. 前回は n≦n*n を sub goal としましたが,今回は結論に含め,帰納法の仮定を強くしました. g `!n. &0 <= &n * (&n - &1) * (&n - &2) /\ &0 <= &n * (&n - &1) /\ &1 + &n + &n * (&n - &1) …