diff options
| author | Pierre Roux | 2018-10-14 15:33:31 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:29 +0200 |
| commit | 49c5de7ead9d008d91a63316e6037bcc9c1f1d52 (patch) | |
| tree | dea3c2b04374888bfbdd802742df4199656ae83e /test-suite/micromega | |
| parent | 7e1243a174e28535d9b35b558ed94f1548acd78c (diff) | |
Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)
Diffstat (limited to 'test-suite/micromega')
| -rw-r--r-- | test-suite/micromega/square.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 7266b662fa..9efb81a901 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -54,7 +54,7 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). |