proposition: Lemma absolu_1 : forall x : Z, Z.abs_nat x = 0 -> x = 0%Z.
proof: Proof. intros x H. case (dec_eq x 0). auto. intro H0. apply False_ind. ElimCompare x 0%Z. intro H2. apply H0. elim (Zcompare_Eq_iff_eq x 0%nat). intros H3 H4. auto. intro H2. cut (exists h : nat, Z.abs_nat x = S h). intro H3. case H3. rewrite H. exact O_S. change (x < 0)%Z in H2. set (H3 := Z.lt_gt _ _ H2) in *. elim (Zcompare_Gt_spec _ _ H3). intros x0 H5. cut (exists q : positive, x = Zneg q). intro H6. case H6. intros x1 H7. rewrite H7. unfold Z.abs_nat in |- *. generalize x1. exact ZL4. cut (x = (- Zpos x0)%Z). simpl in |- *. intro H6. exists x0. assumption. rewrite <- (Z.opp_involutive x). exact (f_equal Z.opp H5). intro H2. cut (exists h : nat, Z.abs_nat x = S h). intro H3. case H3. rewrite H. exact O_S. elim (Zcompare_Gt_spec _ _ H2). simpl in |- *. rewrite Zplus_0_r. intros x0 H4. rewrite H4. unfold Z.abs_nat in |- *. generalize x0. exact ZL4. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)