proposition: Lemma absolu_1 : forall x : Z, Z.abs_nat x = 0 -> x = 0%Z.
proof: Proof. intros. case (dec_eq x 0). intro. assumption. intro. apply False_ind. cut ((x < 0)%Z \/ (x > 0)%Z). intro. ElimCompare x 0%Z. intro. cut (x = 0%Z). assumption. cut ((x ?= 0)%Z = Datatypes.Eq -> x = 0%Z). intro. apply H3. assumption. apply proj1 with (B := x = 0%Z -> (x ?= 0)%Z = Datatypes.Eq). change ((x ?= 0)%Z = Datatypes.Eq <-> x = 0%Z) in |- *. apply Zcompare_Eq_iff_eq. intro. cut (exists h : nat, Z.abs_nat x = S h). intro. case H3. rewrite H. exact O_S. change (x < 0)%Z in H2. cut (0 > x)%Z. intro. cut (exists p : positive, (0 + - x)%Z = Zpos p). simpl in |- *. intro. case H4. intros. cut (exists q : positive, x = Zneg q). intro. case H6. intros. rewrite H7. unfold Z.abs_nat in |- *. generalize x1. exact ZL4. cut (x = (- Zpos x0)%Z). simpl in |- *. intro. exists x0. assumption. cut ((- - x)%Z = x). intro. rewrite <- H6. exact (f_equal Z.opp H5). apply Z.opp_involutive. apply Zcompare_Gt_spec. assumption. apply Z.lt_gt. assumption. intro. cut (exists h : nat, Z.abs_nat x = S h). intro. case H3. rewrite H. exact O_S. cut (exists p : positive, (x + - (0))%Z = Zpos p). simpl in |- *. rewrite Zplus_0_r. intro. case H3. intros. rewrite H4. unfold Z.abs_nat in |- *. generalize x0. exact ZL4. apply Zcompare_Gt_spec. assumption. cut ((x < 0)%Z \/ (0 < x)%Z). intro. apply or_ind with (A := (x < 0)%Z) (B := (0 < x)%Z) (P := (x < 0)%Z \/ (x > 0)%Z). intro. left. assumption. intro. right. apply Z.lt_gt. assumption. assumption. apply not_Zeq. assumption. Qed.
imports: Coq(Lia)