no goals
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
ha : a < o
hb : b < o
⊢ op a b < blsub₂ op o
convert lt_lsub.{v, u}
    (fun x : (Quotient.out.{u+2} o).α × (Quotient.out.{u+2} o).α =>
      op (typein.{u} LT.lt x.fst) (typein.{u} LT.lt x.snd))
    (Prod.mk.{u, u} (enum.{u} LT.lt a (by rwa [type_lt])) (enum.{u} LT.lt b (by rwa [type_lt])))
<;> simp only [typein_enum]
no goals
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
ha : a < o
hb : b < o
⊢ a < type LT.lt
rwa [type_lt]
no goals
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
ha : a < o
hb : b < o
⊢ b < type LT.lt
rwa [type_lt]