#m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
#m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
#n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
#m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
#m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
#n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/