diff options
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. |