proposition: Lemma cPairLemma1 : forall a b : nat, (a + b) * S (a + b) + 2 * a = 2 * cPair a b.
proof: Proof. intros a b. unfold cPair in |- *. assert (2 * sumToN (a + b) = (a + b) * S (a + b)) by (induction (a + b); simpl in |- *; lia). lia. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction