le_of_lt_of_le

Stream: general

[Chris Hughes]

Should we prove le_of_lt_of_le so this stuff works?

example {a b c : ℕ} (h : a < b) (h₁ : b ≤ c) : a ≤ c :=
calc a < b : h
   ... ≤ c : h₁

@[trans] lemma le_of_lt_of_le {a b c : ℕ} : a < b → b ≤ c → a ≤ c := sorry

example {a b c : ℕ} (h : a < b) (h₁ : b ≤ c) : a ≤ c :=
calc a < b : h
   ... ≤ c : h₁

[Kevin Buzzard]

I've run into that before

[Kevin Buzzard]

You have to remember to apply le_of_lt before starting the calc :-)

[Kevin Buzzard]

I like the idea.

[Kevin Buzzard]

dammit I want the proof to be le_of_lt $ lt_of_lt_of_le

[Kevin Buzzard]

:-)

[Kevin Buzzard]

λ x y, le_of_lt $ lt_of_lt_of_le x y looks like you're missing a trick