no goals
α : Type ?u.257723
β : Type ?u.257726
γ : Type ?u.257729
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : a < b
⊢ a % b = a
simp only [mod_def, div_eq_zero_of_lt h, mul_zero, sub_zero]