proposition: Lemma le_0_plus_compat (x y: T): le 0 x → le 0 y → le 0 (x + y).
proof: Proof. Proof with auto. destruct x, y... simpl. intros. apply Qplus_nonneg... Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid Coq.Arith.Arith CoRN.model.rings.Qring CoRN.model.structures.QposInf CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra MathClasses.implementations.stdlib_rationals MathClasses.theory.setoids