proposition: Lemma boundedSearch3 : forall (P : naryRel 2) (b : nat), boundedSearch P b <= b.
proof: Proof. unfold boundedSearch; intros P b; generalize b at 2 3. induction b0. - cbn; auto. - cbn; destruct (Nat.eq_dec (boundedSearchHelp (P b) b0) b0); auto. case_eq (P b b0); auto. Qed.
imports: hydras(primRec extEqualNat ssrnat_extracts) Coq(Min ArithRing Lia Compare_dec Arith Lia)