proposition: Fact pos2nat_inj n (p q : pos n) : pos2nat p = pos2nat q -> p = q.
proof: Proof. revert q. induction p as [ n | n p IHp ]; intros q; invert pos q; simpl; auto; try discriminate 1. intros H; f_equal; apply IHp; injection H; trivial. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)