proposition: Lemma cPairProjections a: cPair (cPairPi1 a) (cPairPi2 a) = a.
proof: Proof. revert a; assert (H: forall a b : nat, b < sumToN a -> cPair (cPairPi1 b) (cPairPi2 b) = b). { intros a b H; induction a as [| a Hreca]. - simpl in H; elim (Nat.nlt_0_r _ H). - induction (Nat.le_gt_cases (sumToN a) b). assert (searchXY b = a) by (apply cPairProjectionsHelp; auto). unfold cPair in |- *. replace (cPairPi1 b + cPairPi2 b) with a. unfold cPairPi1 in |- *. rewrite H1; now rewrite Nat.sub_add. unfold cPairPi2 in |- *. rewrite H1, Nat.add_comm, Nat.sub_add. auto. unfold cPairPi1 in |- *. rewrite H1. simpl in H. erewrite Nat.add_le_mono_l. rewrite Nat.add_comm, sub_add. apply Compat815.lt_n_Sm_le; auto. rewrite add_comm; apply H; auto. auto. apply Hreca. auto. } intros a; apply H with (S a). apply Nat.lt_le_trans with (S a). apply Nat.lt_succ_diag_r . apply sumToN1. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)