no goals
α : Type ?u.260750
β : Type ?u.260753
γ : Type ?u.260756
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
a0 : a = 0
⊢ a % a = 0
simp only [a0, zero_mod]
no goals
α : Type ?u.260750
β : Type ?u.260753
γ : Type ?u.260756
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
a0 : ¬a = 0
⊢ a % a = 0
simp only [mod_def, div_self a0, mul_one, sub_self]