proposition: Lemma P_of_succ_nat_Zplus (m: nat): Zpos (P_of_succ_nat m) = Z_of_nat m + 1.
proof: Proof. destruct m. reflexivity. simpl. destruct (P_of_succ_nat m); reflexivity. Qed.
imports: Coq.ZArith.ZArith CoRN.stdlib_omissions.P Lia