- |napply conj
- [napply (eq_rect_CProp0_r ?? (λx.λ_. m = x + snd … (iso_nat_nat_union s (m - s (S n')) n')) ??
- (split_big_plus
- (S n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
- (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
- (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))?))
- [##2: napply ad_hoc11]
- napply (eq_rect_CProp0_r ?? (λx.λ_. ? = ? + big_plus x (λ_.λ_:? < x.?) + ?)
- ?? (ad_hoc12 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?))
- [##2: nassumption]
- nwhd in ⊢ (???(?(??%)?));
- nrewrite > (ad_hoc13 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?)
- [##2: nassumption]
+ |@
+ [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
+ nrewrite > (ad_hoc12 …); ##[##2: nassumption]
+ nwhd in ⊢ (????(?(??%)?));
+ nrewrite > (ad_hoc13 …);##[##2: nassumption]