proposition: Lemma positive_Sum_two : forall x y : R, [0] [<] x[+]y -> [0] [<] x or [0] [<] y.
proof: Proof. intros. cut ([--]x [<] [0] or [0] [<] y). intro; inversion_clear X0. left; astepl ([--]([0]:R)); astepr ([--][--]x); apply inv_resp_less; assumption. right; assumption. apply less_cotransitive_unfolded. astepl ([0][-]x); apply shift_minus_less'; assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)