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