- [ 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));
- ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ?
- [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj
- [##2: nassumption
- |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]
- napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
- nwhd in ⊢ (???(?(??%)?));
- napply (eq_rect_CProp0_r ?? (λx.λ_. ? = x + ?) ??
- (plus_n_O (big_plus (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')))))));
- 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 …); // ##]##]