α : Type ?u.188636
β : Type ?u.188639
γ : Type ?u.188642
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
x x' : (Quotient.out o).α
⊢ ¬x' < x ↔ x ≤ x'
α : Type ?u.188636
β : Type ?u.188639
γ : Type ?u.188642
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
x x' : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) x ≤ typein (fun x x_1 => x < x_1) x' ↔ x ≤ x'
rw [typein_le_typein]
no goals
α : Type ?u.188636
β : Type ?u.188639
γ : Type ?u.188642
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
x x' : (Quotient.out o).α
⊢ ¬x' < x ↔ x ≤ x'
exact not_lt