proposition: Lemma zero_lt_posplus1 : forall x : R, [0] [<=] x -> [0] [<] x[+][1].
proof: Proof. intros x zltx. apply leEq_less_trans with x. assumption. exact (less_plusOne x). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)