- [ 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 ]##]##]##]
+ [ 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 …); // ##]##]