lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
/3 width=1 by or_intror, conj/
| #m #n #IH #o
<nminus_succ_bi >nplus_succ_shift #Ho
elim (IH … Ho) -IH -Ho * #_ #H
lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
/3 width=1 by or_intror, conj/
| #m #n #IH #o
<nminus_succ_bi >nplus_succ_shift #Ho
elim (IH … Ho) -IH -Ho * #_ #H