proposition: Lemma get_max_bounded_nat (P : nat -> Prop) x n (LE: x <= n) (SAT: P x) : exists m, m <= n /\ P m /\ forall k, k <= n -> P k -> k <= m.
proof: Proof. destruct get_first_nat with (P := fun x => P (n - x)); desf. exists (n - m); repeat split; ins; eauto; try lia. replace k with (n - (n - k)) in H2; [apply H0 in H2|]; lia. destruct (H (n - x)). replace (n - (n - x)) with x; eauto; lia. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite