Commit a084a817 authored by Raphaël Monat's avatar Raphaël Monat

Added lemma: Qeq_bool is symmetric.

parent 10eef967
......@@ -65,3 +65,18 @@ Lemma equal_naming a b c d:
Proof.
unfold Qplus, Qeq; auto.
Qed.
Lemma Qeq_bool_sym a b:
Qeq_bool a b = Qeq_bool b a.
Proof.
unfold Qeq_bool.
case_eq (Zeq_bool (Qnum a * ' Qden b) (Qnum b * ' Qden a)); intros.
- rewrite <- Zeq_is_eq_bool in H.
rewrite H; symmetry.
rewrite <- Zeq_is_eq_bool; auto.
- apply Zeq_bool_neq in H.
case_eq (Zeq_bool (Qnum b *' Qden a) (Qnum a * ' Qden b)); intros.
+ apply Zeq_is_eq_bool in H0.
rewrite H0 in H; auto.
+ auto.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment