α : Type u_1
β : Type ?u.6930
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a
α : Type u_1
β : Type ?u.6930
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ Reachable (hasse α) a b
rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
no goals
α : Type u_1
β : Type ?u.6930
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a
exact
  reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covby_of_not_isMin hc.1.not_isMin)
    fun c hc => Or.inr <| pred_covby_of_not_isMin hc.1.not_isMin