proposition: Lemma exists_max (cond : nat -> Prop) n : (forall m (LT : m < n), ~ cond m) \/ exists m, m < n /\ cond m /\ forall j, m < j -> j < n -> ~ cond j.
proof: Proof. induction n; [left; ins; lia|]. tertium_non_datur (cond n). right; exists n; splits; ins; lia. desf; [left | right]. ins; rewrite Nat.lt_succ_r, Nat.le_lteq in *; desf; eauto. exists m; splits; ins; eauto. rewrite Nat.lt_succ_r, Nat.le_lteq in *; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription