proposition: Lemma boundedSearch1 : forall (P : naryRel 2) (b x : nat), x < boundedSearch P b -> P b x = false.
proof: Proof. unfold boundedSearch in |- *. intros P b. generalize (P b). intros b0 x H. clear P; induction b as [| b Hrecb]. - cbn in H; elim (Nat.nlt_0_r _ H). - cbn in H. induction (eq_nat_dec (boundedSearchHelp b0 b) b). + rewrite a in Hrecb. induction (eq_nat_dec x b). * rewrite a0. induction (b0 b). -- elim (Nat.lt_irrefl b). rewrite a0 in H. auto. -- auto. * apply Hrecb. induction (b0 b). -- auto. -- assert (H0:x <= b). { apply Compat815.lt_n_Sm_le; auto. } induction (Compat815.le_lt_or_eq _ _ H0). ++ auto. ++ elim b1. ** auto. + apply Hrecb; auto. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)