proposition: Lemma Qlt_le_reg : forall a b c d : Q, Qlt a b -> Qle c d -> Qlt (Qplus a c) (Qplus b d).
proof: Proof. intros a b c d Hab Hcd; rewrite (Qplus_sym a); rewrite (Qplus_sym b); apply Qle_lt_reg; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)