proposition: Lemma Qle_plus_neg_neg : forall x y : Q, Qle x Zero -> Qle y Zero -> Qle (Qplus x y) Zero.
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)