local infix:50 " ≺ " => LE.le

#check 1 ≺ 2

theorem simple : 10 = 10 := rfl