proposition: Lemma cPairProjections1 (a b : nat): cPairPi1 (cPair a b) = a.
proof: Proof. unfold cPair, cPairPi1 in |- *. replace (searchXY (a + sumToN (a + b))) with (a + b). now rewrite Nat.add_sub. symmetry in |- *; apply cPairProjectionsHelp. - simpl in |- *; apply 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)