diff options
Diffstat (limited to 'theories/QArith/Qreduction.v')
| -rw-r--r-- | theories/QArith/Qreduction.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 7ca07f841..ddd9b0a26 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -145,6 +145,7 @@ Qed. Definition Qplus' (p q : Q) := Qred (Qplus p q). Definition Qmult' (p q : Q) := Qred (Qmult p q). +Definition Qminus' x y := Qred (Qminus x y). Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). Proof. @@ -156,6 +157,11 @@ Proof. intros; unfold Qmult' in |- *; apply Qred_correct; auto. Qed. +Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q). +Proof. + intros; unfold Qminus' in |- *; apply Qred_correct; auto. +Qed. + Add Morphism Qplus' : Qplus'_comp. Proof. intros; unfold Qplus' in |- *. @@ -167,3 +173,7 @@ Add Morphism Qmult' : Qmult'_comp. rewrite H; rewrite H0; auto with qarith. Qed. +Add Morphism Qminus' : Qminus'_comp. + intros; unfold Qminus' in |- *. + rewrite H; rewrite H0; auto with qarith. +Qed. |