proposition: Lemma find_max_sat2 (f : nat -> bool) n (F: f 0) (G: f (S n) = false) : f (find_max f n) /\ f (S (find_max f n)) = false.
proof: Proof. induction n; ins; desf; eauto. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase