elim (IH (s2-⫯[h]s1)) -IH
[3: /3 width=1 by next_lt, monotonic_lt_minus_r/ ]
>minus_minus_m_m [2,4: /2 width=1 by lt_to_le/ ] -Hs21
elim (IH (s2-⫯[h]s1)) -IH
[3: /3 width=1 by next_lt, monotonic_lt_minus_r/ ]
>minus_minus_m_m [2,4: /2 width=1 by lt_to_le/ ] -Hs21