have : (10591:ℤ) %3 = 1 :=by norm_num
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1
case right.succ.intro.intro.intro.intro.intro.intro.intro.left
a b✝ c : ℤθ
b : ℕ
c1 c2 c3 : ℤ
this : 10591 % 3 = 1
⊢ ((10591 % 3 + c1 % 3 * (31773 % 3) % 3) % 3 + (c3 % 3 * (5184 % 3) % 3 - c2 % 3 * (12834 % 3) % 3) % 3) % 3 = 1