proposition: Lemma eq_true_iff_eq : forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2.
proof: Proof. intros b1 b2; destruct b1,b2 ; intuition congruence. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat