proposition: Theorem Zabs_nat_0 : forall x:Z, Z.abs_nat x = 0 -> (x = 0)%Z.
proof: Proof. intros x; case x. - simpl; auto. - intros p Heq; elim (Nat.lt_irrefl 0). pattern 0 at 2; rewrite <- Heq. simpl; apply lt_O_nat_of_P. - intros p Heq; elim (Nat.lt_irrefl 0). pattern 0 at 2; rewrite <- Heq. simpl; apply lt_O_nat_of_P. Qed.
imports: ZArith Arith Lia