proposition: Lemma cPairLt1 (a b : nat): a < cPair a (S b).
proof: Proof. unfold cPair in |- *. rewrite (Nat.add_comm a (S b)); simpl in |- *. rewrite Nat.add_comm; simpl in |- *; rewrite Nat.add_comm. apply le_n_S, Nat.le_add_r. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)