proposition: Lemma multLemma2 : forall a b : nat, a * b <> 0 -> b <> 0.
proof: Proof. intros a b H; rewrite Nat.mul_comm in H; eapply multLemma1, H. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)