proposition: Lemma lt_iff_S_le x y : x < y ↔ 1 + x ≤ y.
proof: Proof. rewrite commutativity. now apply 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