proposition: Lemma plus_one_ext_less : forall x y : R, x [<] y -> x [<] y[+][1].
proof: Proof. intros x y H. apply less_leEq_trans with y. assumption. apply less_leEq; apply less_plusOne. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)