2013-04-18から1日間の記事一覧
前回の性質を少し一般化したものの tactics による証明です.まず(その1)として,有理数が既約分数で表せることを定理にしておきます. # g `!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`;; val it : goalstack = 1 subgoa…
前回の性質を少し一般化したものの tactics による証明です.まず(その1)として,有理数が既約分数で表せることを定理にしておきます. # g `!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`;; val it : goalstack = 1 subgoa…