proposition: Lemma p_is_some_anti_convert : forall p : positive, exists n : nat, p = P_of_succ_nat n.
proof: Proof. intro p. exists (pred (nat_of_P p)). apply anti_convert_pred_convert. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid