proposition: Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x=y.
proof: Proof. unfold Qcle, Qclt; intros x y H. destruct (Qle_lt_or_eq _ _ H); [left|right]; trivial. now apply Qc_is_canon. Qed.
imports: Field QArith Znumtheory Eqdep_dec