proposition: Lemma Qlt_le_weak : forall x y : Q, Qlt x y -> Qle x y.
proof: Proof. intros x y H. unfold Qle in |- *. intro H2; apply Qlt_irreflexive with x; apply Qlt_transitive with y; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)