diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-02-26 20:16:00 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-02-26 20:18:49 +0100 |
| commit | 3246b4fd3d03cba93c556986ed1a0f9629e4bb73 (patch) | |
| tree | 21a4ba13706a174427f9e438b1927ab0103bb9ae /theories/QArith/Qcanon.v | |
| parent | 20adaabfa96744442f201287e2900b1575614577 (diff) | |
Qcabs : absolute value on normalized rational numbers Qc
File contributed by Cédric Auger (a long time ago, sorry!)
Qarith and Qc would probably deserve many more results like this one,
and a more modern style (for instance qualified names), but this commit
is better than nothing...
Diffstat (limited to 'theories/QArith/Qcanon.v')
| -rw-r--r-- | theories/QArith/Qcanon.v | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 078926e32..6bfa47bc5 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -81,14 +81,6 @@ Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). Arguments Q2Qc q%Q. -Lemma Qred_eq_iff (q q' : Q) : Qred q = Qred q' <-> q == q'. -Proof. - split. - - intros E. rewrite <- (Qred_correct q), <- (Qred_correct q'). - now rewrite E. - - apply Qred_complete. -Qed. - Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. Proof. split; intro H. @@ -488,7 +480,7 @@ Proof. destruct n; simpl. destruct 1; auto. intros. - now apply Qc_is_canon. + now apply Qc_is_canon. Qed. Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. |