feat(data/rat): redefine rat.lt so that apply works

[robertylewis]

I noticed the following a little while ago, and worked around it, but it came up again.

import data.rat

theorem f2 (T : Type) (h : ordered_comm_group T) : (0 : T) < 0 := sorry

example : (0 : ℤ) < 0 :=
begin 
apply f2
end

example : (0 : ℚ) < 0 :=
begin 
apply f2 -- fails
end

When apply chooses how many arguments to instantiate with metavariables, it does some unfolding. When lt is defined as the negation of le, the count is off by one and apply fails. There are other possible fixes, I think, but this one works for now.

This is based on 3.3.0 since I'm working with that version right now, but I think the same patch should apply to master; I don't remember how we decided to handle these kinds of fixes.

[digama0]

The latest commit resolves this issue by using the default implementation of lt. The reason it was implemented that way in the first place was so that the decidable instance wouldn't have to calculate two le relations, but that can be done (and is now done) in the decidable instance itself.

[robertylewis]

@digama0 Thanks. Would it be possible to apply this fix (or your version of this fix, it doesn't matter) to the v3.3.0 branch? I want to keep this project on a stable version.

[digama0]

Backported