proposition: Lemma natTimes (a b : nat): SysPrf NN (natToTerm a *natToTerm b = natToTerm (a * b)%nat)%fol.
proof: Proof. - induction b as [| b Hrecb]. + rewrite Nat.mul_comm; cbn; apply nn5. + rewrite Nat.mul_comm; cbn; eapply eqTrans. * apply nn6. * rewrite Nat.add_comm; apply eqTrans with (natToTerm (b * a)%nat + natToTerm a)%fol. -- apply eqPlus. ++ rewrite Nat.mul_comm; apply Hrecb. ++ apply eqRefl. -- apply natPlus. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)