proposition: Lemma lt_abs_abs : forall (n m : int), (0 <= n) -> (n < m) -> (abs n < abs m).
proof: Proof. Proof using. intros. nat_comp_to_peano. apply Zabs_nat_lt. math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)