proposition: Lemma cPairLt2 (a b : nat): b < cPair (S a) b.
proof: Proof. unfold cPair in |- *; simpl in |- *; unfold lt in |- *; apply le_n_S. eapply Nat.le_trans. - apply Nat.le_add_r. - rewrite Nat.add_comm at 1. apply Nat.add_le_mono_l. apply le_S. eapply Nat.le_trans. + apply Nat.le_add_r. + rewrite Nat.add_comm; apply Nat.le_add_r. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)