#m elim m -m [ #n #i #H elim (lt_zero_false … H) ]
#m #IH #n * [ /2 width=2 by refl, at_refl/ ]
#i #H lapply (lt_S_S_to_lt … H) -H /3 width=7 by refl, at_push/
qed.
#m elim m -m [ #n #i #H elim (lt_zero_false … H) ]
#m #IH #n * [ /2 width=2 by refl, at_refl/ ]
#i #H lapply (lt_S_S_to_lt … H) -H /3 width=7 by refl, at_push/
qed.