- [ napply conj [napply conj; //;
- nwhd in ⊢ (???(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); //
- ##| nnormalize; // ]
-##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
- nlapply (Hrec (m - s (S n')) ?); /2/; *; *; #Hrec1; #Hrec2; #Hrec3; @; //; @; /2/;
- nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
- nrewrite > (ad_hoc12 …); //;
- nwhd in ⊢ (???(?(??%)?));
- nrewrite > (ad_hoc13 …); //;
- napply ad_hoc14; /2/;
- nwhd in ⊢ (???(?(??%)?));
- nrewrite > (plus_n_O …); // ##]##]
+ [ napply conj [napply conj
+ [ nwhd in ⊢ (???(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
+ | nnormalize; napply le_n]
+ ##| nnormalize; nassumption ]
+ ##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
+ nlapply (Hrec (m - s (S n')) ?)
+ [ napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; @
+ [##2: nassumption
+ |@
+ [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
+ nrewrite > (ad_hoc12 …); ##[##2: nassumption]
+ nwhd in ⊢ (???(?(??%)?));
+ nrewrite > (ad_hoc13 …);##[##2: nassumption]
+ napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
+ nwhd in ⊢ (???(?(??%)?));
+ nrewrite > (plus_n_O …);
+ nassumption;
+ ##| napply le_S; nassumption ]##]##]##]