proposition: Fact pos_list_prop n p : In p (pos_list n).
proof: Proof. induction p as [ | n p Hp ]. left; auto. simpl; right. apply in_map_iff. exists p; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)