case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h✝ : a ⩿ b
h : a ⋖ b
⊢ b ≤ succ a

case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
h : a ⩿ a
⊢ a ≤ succ a
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a
obtain h | rfl := h.covby_or_eq
no goals
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
h✝ : a ⩿ b
h : a ⋖ b
⊢ b ≤ succ a
exact (Covby.succ_eq h).ge
no goals
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
h : a ⩿ a
⊢ a ≤ succ a
exact le_succ _