proposition: Lemma mult_correct: PRcorrect mult Nat.mul.
proof: Proof. intro n; induction n as [ | n IHn]. - intro p; reflexivity. - intro p; rewrite mult_eqn1, (IHn p) , plus_correct. cbn. ring. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)