proposition: Fact list_an_spec a n m : In m (list_an a n) <-> a <= m < a+n.
proof: Proof. revert a; induction n as [ | n IHn ]; simpl; intros a; [ | rewrite IHn ]; lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)