-| #m #IH #n @(nat_ind … n) -n
- [ #o #Ho
- lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
- /3 width=1 by or_intror, conj/
- | #n #_ #o
- <nminus_succ_bi >nplus_succ_shift #Ho
- elim (IH … Ho) -IH -Ho * #_ #H
- elim (eq_inv_nzero_succ … H)
- ]
+| #m #o #Ho
+ 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
+ elim (eq_inv_nzero_succ … H)