proposition: Lemma le_iff_lt_plus_1 x y : x ≤ y ↔ x < y + 1.
proof: Proof. split; intros E. apply lt_iff_plus_1_le. now apply (order_preserving (+1)). now apply (order_reflecting (+1)), lt_iff_plus_1_le. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals MathClasses.orders.semirings