proposition: Lemma ZL9 : forall p : positive, Z_of_nat (nat_of_P p) = Zpos p.
proof: Proof. intro. cut (exists h : nat, nat_of_P p = S h). intro. case H. intros. unfold Z_of_nat in |- *. rewrite H0. apply f_equal with (A := positive) (B := Z) (f := Zpos). cut (P_of_succ_nat (nat_of_P p) = P_of_succ_nat (S x)). intro. rewrite P_of_succ_nat_o_nat_of_P_eq_succ in H1. cut (Pos.pred (Pos.succ p) = Pos.pred (P_of_succ_nat (S x))). intro. rewrite Pos.pred_succ in H2. simpl in H2. rewrite Pos.pred_succ in H2. apply sym_eq. assumption. apply f_equal with (A := positive) (B := positive) (f := Pos.pred). assumption. apply f_equal with (f := P_of_succ_nat). assumption. apply ZL4. Qed.
imports: Coq(Lia)