α : Type ?u.254011
β : Type ?u.254014
γ : Type ?u.254017
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b : Ordinal
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b
α : Type ?u.254011
β : Type ?u.254014
γ : Type ?u.254017
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h₁ : a ∣ b
h₂ : b ∣ a
a0 : a = 0
⊢ a = b
subst a
no goals
α : Type ?u.254011
β : Type ?u.254014
γ : Type ?u.254017
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
b : Ordinal
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b
exact (eq_zero_of_zero_dvd h₁).symm
α : Type ?u.254011
β : Type ?u.254014
γ : Type ?u.254017
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0
α : Type ?u.254011
β : Type ?u.254014
γ : Type ?u.254017
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h₁ : a ∣ b
h₂ : b ∣ a
a0 : ¬a = 0
b0 : b = 0
⊢ a = b
subst b
no goals
α : Type ?u.254011
β : Type ?u.254014
γ : Type ?u.254017
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0
exact eq_zero_of_zero_dvd h₂