proposition: Lemma lt_to_nat_to_nat : forall (n m : int), (0 <= n) -> (n < m) -> (to_nat n < to_nat m).
proof: Proof. Proof using. intros. nat_comp_to_peano. rewrite <-!Zabs2Nat.abs_nat_nonneg by math. apply~ Zabs_nat_lt. math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)