rfl vs dec_trivial for inequality example

Stream: new members

[Joseph Corneli]

This works:

theorem one_plus_one_alt : 1 + 1 = 2 := rfl

example : 1 + 1 ≤ 2 := dec_trivial

This doesn't work:

example : 1 + 1 ≤ 2 := rfl

:confused:

[Rob Lewis]

Look at the type of rfl? It proves equality, not inequality.

[Rob Lewis]

You might be looking for le_refl.