proposition: Theorem Q_eq_prop : forall x y : Q, Q_eq x y = true -> x = y.
proof: Proof. intros x y Htrue; generalize Htrue; clear Htrue. case y; case x; try (intros; simpl in Htrue; discriminate; fail). auto. intros x' y'; simpl in |- *; case (Qpositive_eq_dec x' y'). intros H; rewrite H; auto. intros; discriminate. intros x' y'; simpl in |- *; case (Qpositive_eq_dec x' y'). intros H; rewrite H; auto. intros; discriminate. Qed.