proposition: Theorem le_lteq : forall x y : t, le x y <-> lt x y \/ eq x y.
proof: Proof. intros x y. unfold le,lt,eq. split; intro H. destruct (Qcle_lt_or_eq _ _ H). now left. right. assumption. destruct H. now apply Qlt_le_weak. subst. now apply Qcle_refl. Qed.
imports: QArith_base Qcanon Equalities Orders OrdersTac