proposition: Lemma cPairLe2A (a: nat): cPairPi2 a <= a.
proof: Proof. transitivity (cPair (cPairPi1 a) (cPairPi2 a)). - apply cPairLe2. - rewrite cPairProjections; apply le_n. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)