proposition: Lemma set_finite_lt n : set_finite (fun t => t < n).
proof: Proof. exists (List.seq 0 n); intros; apply in_seq; ins; auto with arith. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms