deniok

Эти ваши интернеты бурлят:

ru-marazm.livejournal.com/3591670.html

lj.rossia.org/users/tiphareth/1685303.html

Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:

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

Впрочем внучке стоило бы снять все вопросы, предоставив доказательство

*-commutative : ∀ m n → m * n ≡ n * m

Взяв его, например, из Data.Nat.Properties. Или получив самостоятельно.