proposition: Lemma cPairProjectionsHelp (a b: nat): b < sumToN a.+1 -> sumToN a <= b -> searchXY b = a.
proof: Proof. intros H H0; unfold searchXY in |- *. induction (boundedSearch2 (fun b y : nat => ltBool b (sumToN y.+1)) b). - rewrite H1. induction (eq_nat_dec b a). + auto. + elim (ltBoolFalse b (sumToN a.+1)). * apply (boundedSearch1 (fun b y : nat => ltBool b (sumToN y.+1)) b). rewrite H1. destruct (Nat.lt_gt_cases b a) as [H2 _]; specialize (H2 b0); destruct H2 as [H2 | H2]. -- rewrite Nat.lt_nge in H2. destruct H2. apply Nat.le_trans with (sumToN a). apply sumToN1. auto. -- auto. * auto. - set (c := boundedSearch (fun b y : nat => ltBool b (sumToN y.+1 )) b) in *. induction (eq_nat_dec c a). + auto. + elim (ltBoolFalse b (sumToN a.+1)). apply (boundedSearch1 (fun b y : nat => ltBool b (sumToN y.+1)) b). fold c in |- *. rewrite lt_gt_cases in b0; destruct b0 as [H2 | H2]; [trivial|]. rewrite Nat.le_ngt in H0; destruct H0. * apply Nat.lt_le_trans with (sumToN c.+1). -- apply ltBoolTrue. auto. -- assert (c.+1 <= a). { apply Compat815.lt_n_Sm_le. now rewrite <- Nat.succ_lt_mono. } apply sumToN2; auto. * assumption. * assumption. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)