§2.5: explain how to call inf_le_left when arguments are not inferrable

[darijgr]

The claim that

Of course you can also avoid this issue by providing directly a full proof such as
exact le_trans inf_le_left inf_le_right, but this requires a lot more
planning.
is rather misleading: In the form given above, the proof does not compile, and inf_le_left has both of its arguments implicit, which makes it unusable with what has been covered so far in the text.

I have replaced it by

exact le_trans (inf_le_left : (x ⊓ y) ⊓ z ≤ x ⊓ y) (inf_le_right : x ⊓ y ≤ y);
which has the advantage of showing how type inference can be given a helping hand.