proposition: Lemma POS_anti_convert : forall n : nat, S n = Zpos (P_of_succ_nat n) :>Z.
proof: Proof. simple induction n. simpl in |- *. reflexivity. intros n0 H. simpl in |- *. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid