proposition: Fact pos2nat_right n m p : pos2nat (@pos_right n m p) = n+pos2nat p.
proof: Proof. revert m p; induction n as [ | n IHn ]; intros m p; auto. simpl pos_right; simpl plus; rewrite pos2nat_nxt; f_equal; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)