proposition: Lemma Qle_plus_pos_pos : forall x y : Q, Qle Zero x -> Qle Zero y -> Qle Zero (Qplus x y).
proof: Proof. intros b d Hb Hd; replace Zero with (Qplus Zero Zero); trivial; apply Qle_plus_plus; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)