proposition: Theorem nat_to_Z_and_back: forall n:nat, Z.abs_nat (Z_of_nat n) = n.
proof: Proof. intros n; elim n. - auto. - intros n'; simpl; case n'. + simpl; auto. + intros n''; simpl; rewrite nat_of_P_Psucc; intros Heq; rewrite Heq; auto. Qed.
imports: ZArith Arith Lia