| <(nle_inv_eq_zero_minus m21 ?) // <nplus_zero_sn <nminus_plus_assoc <nplus_comm
elim (nat_split_le_ge m11 m21) #Hm121
[ lapply (nle_minus_sn_dx … Hm1121) #Hm2112
| <(nle_inv_eq_zero_minus m21 ?) // <nplus_zero_sn <nminus_plus_assoc <nplus_comm
elim (nat_split_le_ge m11 m21) #Hm121
[ lapply (nle_minus_sn_dx … Hm1121) #Hm2112