Вот в Agda, например:

_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = (m * n) + n

m-zero-right : (n : ℕ) → n * 0 ≡ 0
m-zero-right zero = refl
m-zero-right (suc n) = trans (sym (p-zero-right (n * 0))) (m-zero-right n)

m-nsm : (n m : ℕ) → m * (suc n) ≡ (m * n) + m
m-nsm n zero = refl
m-nsm n (suc m) with m-nsm n m
m-nsm n (suc m) | eq = begin
suc m * suc n
≡⟨ refl ⟩
((m * suc n) + (suc n))
≡⟨ cast-gen (λ x → m * suc n + suc n ≡ x + suc n) eq refl ⟩
m * n + m + suc n
≡⟨ trans (p-assoc (m * n) m (suc n)) refl ⟩
(m * n + (m + suc n))
≡⟨ (cast-gen (λ x → m * n + (m + suc n) ≡ m * n + x) (sym (p-snm-nsm m n)) refl) ⟩
(m * n + (suc m + n))
≡⟨ (cast-gen (λ x → m * n + (suc m + n) ≡ m * n + x) (p-comm (suc m) n) refl) ⟩
(m * n + (n + suc m))
≡⟨ (trans (sym (p-assoc (m * n) n (suc m))) refl) ⟩
(m * n + n + suc m ∎)

m-comm : (n m : ℕ) → n * m ≡ m * n
m-comm n zero = m-zero-right n
m-comm n (suc m) with m-comm n m
m-comm n (suc m) | eq = trans (m-nsm m n) (cast-gen (λ (x : ℕ) → x + n ≡ m * n + n) (sym eq) refl)