diff options
| author |  roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-21 11:46:13 +0000 |
|---|---|---|
| committer | roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-21 11:46:13 +0000 |
| commit | bd5b2a45c2ef00d63fc84f5f1bc577fcb3a3d0d9 (patch) | |
| tree | 635e016228fd284c8f4165465b728f0c8cc48aa3 /theories/QArith/Qreduction.v | |
| parent | f4586d1e8b1116340574d9660117f93e7a1e4e3b (diff) | |
Adding: Field instance for Q.
: Power function from Q -> Z -> Q.
: Absolute value function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
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. |