Theorem: mod_mod (ECTate/Algebra/ValuedRing.lean)

State before:
K : Type u_1
a b : K
inst✝ : EuclideanDomain K
⊢ a % b % b = a % b
Tactic:
sorry
State after:
no goals