proposition: Theorem eq_dec : ∀ a b, {qeq a b} + {not (qeq a b)}.
proof: Proof. intros a b. destruct a as [a| ]; simpl. destruct b as [b| ]; simpl. apply Qeq_dec. right; intros H; assumption. destruct b as [b| ]. right; intros H; assumption. left; constructor. Qed.
imports: Utf8 QArith Misc