proposition: Lemma eq_inj : forall m n : nat, m = n :>Z -> m = n.
proof: Proof. intros. generalize (f_equal Z.abs_nat H). intro. rewrite (absolu_inject_nat m) in H0. rewrite (absolu_inject_nat n) in H0. assumption. Qed.
imports: Coq(Lia)