α : Type u_1
β : Type ?u.5179
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b
α : Type u_1
β : Type ?u.5179
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ Reachable (hasse α) a b
rw [reachable_iff_reflTransGen]
no goals
α : Type u_1
β : Type ?u.5179
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b
exact
  reflTransGen_of_succ _ (fun c hc => Or.inl <| covby_succ_of_not_isMax hc.2.not_isMax)
    fun c hc => Or.inr <| covby_succ_of_not_isMax hc.2.not_isMax