proposition: Lemma plus_resp_pos_nonneg : forall x y : R, [0] [<] x -> [0] [<=] y -> [0] [<] x[+]y.
proof: Proof. intros. apply less_leEq_trans with x. auto. astepl (x[+][0]). apply plus_resp_leEq_lft. auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)