[rewrite > H;rewrite > H in Hletin;simplify;constructor 1
|rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
unfold;apply le_S_S;assumption]
[rewrite > H;rewrite > H in Hletin;simplify;constructor 1
|rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
unfold;apply le_S_S;assumption]