proposition: Lemma absolu_2 : forall x : Z, x <> 0%Z -> Z.abs_nat x <> 0.
proof: Proof. intros x H. intro H0. apply H. apply absolu_1. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)