diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-03 16:20:08 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-03 16:20:08 +0200 |
| commit | dfa56fb57b09296cdf311ec5972d2d33b787e48c (patch) | |
| tree | 301e2b657d89a7edd98c38bf8428a88a99720652 /theories | |
| parent | d4009edb53ab7780bc85d83ccf01c6920c7f09e1 (diff) | |
Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/Qabs.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 116aa0d42..ec2ac7832 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -100,6 +100,13 @@ rewrite Z.abs_mul. reflexivity. Qed. +Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q). +Proof. + intros [n d]; simpl. + unfold Qinv. + case_eq n; intros; simpl in *; apply Qeq_refl. +Qed. + Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). Proof. unfold Qminus, Qopp. simpl. |