α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m
rw [← reflTransGen_swap]
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n
exact reflTransGen_of_succ_of_le (swap r) h hmn