`BookProof.ChapterFiniteArithmeticPrior.truncMul_saturates` {B : ℕ} [NeZero B] (a b : Fin B) (h : ¬ (a : ℕ) * (b : ℕ) < B) : (((truncMul B).result a b : Fin B) : ℕ) = B

Initializing...

`BookProof.ChapterFiniteArithmeticPrior.truncMul_saturates` {B : ℕ} [NeZero B] (a b : Fin B) (h : ¬ (a : ℕ) * (b : ℕ) < B) : (((truncMul B).result a b : Fin B) : ℕ) = B - 1 · Prove2Me