proposition: Lemma Qle_lt_reg : forall a b c d : Q, Qle a b -> Qlt c d -> Qlt (Qplus a c) (Qplus b d).
proof: Proof. intros a b c d Hab Hcd. case (Qle_lt_eq_dec _ _ Hab); intro Hab'; [ apply Qlt_plus_plus | rewrite Hab'; unfold Qlt in |- *; apply Qgt_plus ]; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)