@[to_dual] attributes for basic types

theorem le_of_eq_of_le'' {α : Type u_1} {a b c : α} [LE α] (h₁ : a = b) (h₂ : c ≤ b) : c ≤ a

theorem le_of_le_of_eq'' {α : Type u_1} {a b c : α} [LE α] (h₁ : b ≤ a) (h₂ : b = c) : c ≤ a

theorem lt_of_eq_of_lt'' {α : Type u_1} {a b c : α} [LT α] (h₁ : a = b) (h₂ : c < b) : c < a

theorem lt_of_lt_of_eq'' {α : Type u_1} {a b c : α} [LT α] (h₁ : b < a) (h₂ : b = c) : c < a