proposition: Fact pos2nat_nat2pos n i (H : i < n) : pos2nat (nat2pos H) = i.
proof: Proof. revert i H; induction n as [ | n IHn ]; intros [ | i ] H; simpl; auto; try lia. f_equal. apply IHn. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)