proposition: Lemma Qlt_plus_plus : forall a b c d : Q, Qlt a b -> Qlt c d -> Qlt (Qplus a c) (Qplus b d).
proof: Proof. intros a b c d Hab Hcd. apply Qlt_transitive with (Qplus b c); unfold Qlt in |- *; [ rewrite (Qplus_sym a); rewrite (Qplus_sym b) | idtac ]; apply Qgt_plus; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)