proposition: Lemma cPairLe2 (a b : nat) : b <= cPair a b.
proof: Proof. unfold cPair in |- *; eapply Nat.le_trans with (b + a). - apply Nat.le_add_r. - rewrite (Nat.add_comm b a); transitivity (sumToN (a + b)). + apply sumToN1. + rewrite (Nat.add_comm _ (sumToN (a + b))); apply le_add_r. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)