let lem1 = SIMP_RULE [REAL_POW2_ABS; REAL_INJ; REAL_MUL] (REAL_FIELD `~(&q = &0) ==> abs x = &p / &q ==> ~(&(gcd (p,q)) = &0) ==> &p = &a' * &(gcd (p,q)) ==> &q = &b' * &(gcd (p,q)) ==> &a' * &a' = abs x pow 2 * &b' * &b'`);; let RATIONAL_…

以下，表題の証明です． # g `!s. prime s ==> ~rational (sqrt (&s))` ;; val it : goalstack = 1 subgoal (1 total) `!s. prime s ==> ~rational (sqrt (&s))` まず，全称量化を外し，前件を仮定に廻して，結論を（その１）の定理でリライトします． # e( …