proposition: Lemma succ_nat: forall (m:nat),Zpos (P_of_succ_nat m) = (Z_of_nat m + 1)%Z.
proof: Proof. intro m. induction m. reflexivity. simpl. case (P_of_succ_nat m). simpl. reflexivity. simpl. reflexivity. simpl. reflexivity. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)