proposition: Fact pos_sub2nat n p m Hm : pos2nat (@pos_sub n p m Hm) = pos2nat p.
proof: Proof. revert m Hm; induction p as [ n | n p IH ]; intros [ | m ] Hm; try lia. simpl; auto. simpl pos_sub; repeat rewrite pos2nat_nxt; f_equal; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)