Why unfold does not work on lt(less-than) in Coq? -

i'd prove lt n m -> le n m since not exist in coq's standard library.

though in coq.init.peano, lt m n defined s m <= n, cannot unfold lt in hypothesis use such definition.

why unfold not work? seems inversion work.

i don't know version of coq using, on mine, unfold works fine: if unfold lt in h. in

1 subgoal n : nat m : nat h : n < m ______________________________________(1/1) n <= m 

i following goal:

1 subgoal n : nat m : nat h : s n <= m ______________________________________(1/1) n <= m 

by way, lemma looking in nat.lt_le_incl.