proposition: Lemma cPairProjections2 (a b : nat): cPairPi2 (cPair a b) = b.
proof: Proof. unfold cPairPi2 in |- *; rewrite cPairProjections1; unfold cPair in |- *. replace (searchXY (a + sumToN (a + b))) with (a + b). - rewrite Nat.add_comm; apply Nat.add_sub . - symmetry in |- *; apply cPairProjectionsHelp; simpl in |- *. + rewrite Nat.lt_succ_r; apply Nat.add_le_mono_r, Nat.le_add_r. + rewrite (Nat.add_comm a (sumToN (a + b)));apply le_add_r. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)