proposition: Lemma int_to_nat_lt x y : 0 < y → x < y → int_to_nat Z N x < int_to_nat Z N y.
proof: Proof. intros Ey Exy. destruct (total (≤) 0 x). now apply int_to_nat_lt_cancel_r, int_to_nat_lt_l. rewrite int_to_nat_of_nonpos by easy. now apply int_to_nat_pos. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings