proposition: Lemma cPairLe3 (a b c d : nat): a <= b -> c <= d -> cPair a c <= cPair b d.
proof: Proof. intros H H0; unfold cPair in |- *; transitivity (a + sumToN (b + d)). - apply Nat.add_le_mono_l, sumToN2; transitivity (a + d). + now apply Nat.add_le_mono_l. + now apply Nat.add_le_mono_r. - now apply Nat.add_le_mono_r. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)