proposition: Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y.
proof: Proof. intros x y; unfold Qc_eq_bool; case (Qc_eq_dec x y); simpl; auto. intros _ H; inversion H. Qed.
imports: Field QArith Znumtheory Eqdep_dec