case inl
α : Type ?u.265351
β : Type ?u.265354
γ : Type ?u.265357
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
y z : Ordinal
⊢ (0 * y + z) % 0 = z % 0

case inr
α : Type ?u.265351
β : Type ?u.265354
γ : Type ?u.265357
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x y z : Ordinal
hx : x ≠ 0
⊢ (x * y + z) % x = z % x
α : Type ?u.265351
β : Type ?u.265354
γ : Type ?u.265357
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x y z : Ordinal
⊢ (x * y + z) % x = z % x
rcases eq_or_ne x 0 with rfl | hx
no goals
case inl
α : Type ?u.265351
β : Type ?u.265354
γ : Type ?u.265357
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
y z : Ordinal
⊢ (0 * y + z) % 0 = z % 0
simp
no goals
case inr
α : Type ?u.265351
β : Type ?u.265354
γ : Type ?u.265357
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x y z : Ordinal
hx : x ≠ 0
⊢ (x * y + z) % x = z % x
rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]