diff options
| author | Erik Martin-Dorel | 2020-05-04 14:23:58 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2020-05-04 14:23:58 +0200 |
| commit | 3bc39fbd726676e5d1a650b683f0b5d72dbd1c3b (patch) | |
| tree | 5a41abd27b293b4d18b66b3ef1c5484ecf59f23b /ci/test_wholefile.v | |
| parent | 866a9da96a53c387050e7d8f7df9a0a3e35b435f (diff) | |
fix: Tweak comments and workaround ProofGeneral/PG#485
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*) |