proposition: Lemma set_finite_nat_bounded s (F : set_finite s) : (exists bound, forall m (M: s m), m < bound).
proof: Proof. red in F; desc. exists (S (fold_right Nat.max 0 findom)); ins. apply Nat.lt_succ_r. apply F, in_split in M; desf. clear; induction l1; ins; eauto 2 with arith. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms