proposition: Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.
proof: Proof. rewrite !Qeq_bool_iff; apply Qeq_trans. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool