proposition: Fact pos_list2nat n : map (@pos2nat n) (pos_list n) = list_an 0 n.
proof: Proof. induction n as [ | n IHn ]; simpl; f_equal. rewrite <- (map_S_list_an 0), <- IHn. do 2 rewrite map_map. apply map_ext. intros; rewrite pos2nat_nxt; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)