diff options
| author | Erik Martin-Dorel | 2020-05-04 14:54:43 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2020-05-04 14:54:43 +0200 |
| commit | 6f2f532af7d065779bca1e7c994d065f50338d9c (patch) | |
| tree | f3d008a5da93a0fab2d0f0b3035a10e81d1efb6f /ci/test_wholefile.v | |
| parent | 395f6f076ed4061417b4a5747797dab413ad2453 (diff) | |
test: Remove "Proof." workaround
Diffstat (limited to 'ci/test_wholefile.v')
| -rw-r--r-- | ci/test_wholefile.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v index d8b57d20..f947d1c5 100644 --- a/ci/test_wholefile.v +++ b/ci/test_wholefile.v @@ -133,7 +133,6 @@ 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. |