proposition: Lemma Qc_dec : forall x y, {x<y} + {y<x} + {x=y}.
proof: Proof. unfold Qclt, Qcle; intros. destruct (Q_dec x y) as [H|H]. - left; auto. - right; apply Qc_is_canon; auto. Defined.
imports: Field QArith Znumtheory Eqdep_dec