proposition: Lemma invert_nat_fun_sat f y (F : f 0 <= y) : f (invert_nat_fun f y) <= y.
proof: Proof. apply Nat.leb_le, find_max_sat with (f := fun x => f x <=? y) . apply Nat.leb_le; done. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase