case intro
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b c : Ordinal
⊢ b * c % b = 0
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
H : b ∣ a
⊢ a % b = 0
rcases H with ⟨c, rfl⟩
case intro.inl
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Ordinal
⊢ 0 * c % 0 = 0

case intro.inr
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b c : Ordinal
hb : b ≠ 0
⊢ b * c % b = 0
case intro
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b c : Ordinal
⊢ b * c % b = 0
rcases eq_or_ne b 0 with (rfl | hb)
no goals
case intro.inl
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Ordinal
⊢ 0 * c % 0 = 0
simp
no goals
case intro.inr
α : Type ?u.263181
β : Type ?u.263184
γ : Type ?u.263187
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b c : Ordinal
hb : b ≠ 0
⊢ b * c % b = 0
simp [mod_def, hb]