proposition: Lemma ZL9 : forall p : positive, Z_of_nat (nat_of_P p) = Zpos p.
proof: Proof. intro p. elim (ZL4 p). intros x H0. rewrite H0. unfold Z_of_nat in |- *. 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 H1. 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 H2. rewrite Pos.pred_succ in H2. simpl in H2. rewrite Pos.pred_succ in H2. auto. apply f_equal with (A := positive) (B := positive) (f := Pos.pred). assumption. apply f_equal with (f := P_of_succ_nat). assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)