proposition: Theorem nat_of_P_Psucc : forall p:positive, nat_of_P (Pos.succ p) = S (nat_of_P p).
proof: Proof. intros p; elim p. - simpl; intros p'; rewrite nat_of_P_xO. intros Heq; rewrite Heq; rewrite nat_of_P_xI; ring. - intros p' Heq; simpl. rewrite nat_of_P_xI. rewrite nat_of_P_xO;auto. - auto. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv