proposition: Lemma lt_iff_plus_1_le x y : x < y <-> x + 1 ≤ y.
proof: Proof. etransitivity. - apply nat_int_lt_plus. - apply symmetry,nat_int_le_plus. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.naturals HoTT.Classes.theory.rings HoTT.Classes.orders.semirings