proposition: Lemma Qc_eq_bool_iff : forall x y, Qc_eq_bool x y = true <-> x = y.
proof: Proof. intros. split. apply Qc_eq_bool_correct. intro. unfold Qc_eq_bool. destruct (Qc_eq_dec x y). reflexivity. contradiction. Qed.
imports: QArith_base Qcanon Equalities Orders OrdersTac