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