diff options
Diffstat (limited to 'ci/test_wholefile.v')
| -rw-r--r-- | ci/test_wholefile.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v index 0a87d9a6..d8b57d20 100644 --- a/ci/test_wholefile.v +++ b/ci/test_wholefile.v @@ -1,4 +1,4 @@ -(*taking from coq.inria.fr *) +(* taken from https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot.sqrt2.html *) Require Export ArithRing. Require Export Compare_dec. @@ -133,6 +133,7 @@ Hint Resolve lt_le_weak comparison2: sqrt. Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False. +Proof. intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf). clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq)); intros Hlt_O_q Heq. @@ -141,5 +142,3 @@ apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 * p); rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with *. apply new_equality; auto. Qed. - -(*end here*) |