Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful

2 files changed, 27 insertions, 0 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index a19f9f902..5996d30f2 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -171,6 +171,26 @@ Proof.
  auto with qarith.
 Qed.
 
+Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x.
+Proof.
+ apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry.
+Qed.
+
+Lemma Qeq_bool_refl x: Qeq_bool x x = true.
+Proof.
+  rewrite Qeq_bool_iff. now reflexivity.
+Qed.
+
+Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true.
+Proof.
+  rewrite !Qeq_bool_iff. now symmetry.
+Qed.
+
+Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.
+Proof.
+  rewrite !Qeq_bool_iff; apply Qeq_trans.
+Qed.
+
 Hint Resolve Qnot_eq_sym : qarith.
 
 (** * Addition, multiplication and opposite *)
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.