proposition: Lemma get_first_nat (P : nat -> Prop) : (exists m, P m /\ forall k, P k -> m <= k) \/ forall k, ~ P k.
proof: Proof. apply NNPP; intro X; apply not_or_and in X; desf. apply not_all_not_ex in X0; desf; destruct X. revert P X0; induction n; ins. by exists 0; split; ins; desf; auto with arith. destruct (classic (P 0)). by exists 0; split; ins; desf; auto with arith. specialize (IHn (fun n => P (S n)) X0); desf. eexists (S m); split; ins; eauto. destruct k; try done; eauto using le_n_S. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite