- napply (ex_intro … xxx); napply conj
- [ nwhd in Hni1; nwhd; nwhd in ⊢ (?(? %)%);
- nchange with (? < plus (s n) (big_plus n ?));
- nelim (le_to_lt_or_eq … (le_S_S_to_le … Hni1))
- [##2: #E; nrewrite < E; nrewrite < (minus_canc nindex);
- nwhd in ⊢ (?%?); nrewrite < E; napply lt_to_lt_plus; nassumption
- | #L; nrewrite > (split_big_plus n (S nindex) (λm.λ_.s m) L);
- nrewrite > (split_big_plus (n - nindex) (n - S nindex) (λi.λ_.s (S (i+nindex))) ?)
- [ ngeneralize in match (big_plus_ext (n - S nindex)
- (λi,p.s (S (i+nindex))) (λi,p.s (i + S nindex)) ?) in ⊢ ?
- [ #E;
- napply (eq_rect_CProp0_r ??
- (λx:nat.λ_. x + big_plus (n - nindex - (n - S nindex))
- (λi,p.s (S (i + (n - S nindex)+nindex))) + nindex2 <
- s n + (big_plus (S nindex) (λi,p.s i) +
- big_plus (n - S nindex) (λi,p. s (i + S nindex)))) ? ? E);
- nrewrite > (ad_hoc1 (s n) (big_plus (S nindex) (λi,p.s i))
- (big_plus (n - S nindex) (λi,p. s (i + S nindex))));
- napply (eq_rect_CProp0_r
- ?? (λx.λ_.x < ?) ?? (assoc
- (big_plus (n - S nindex) (λi,p.s (i + S nindex)))
- (big_plus (n - nindex - (n - S nindex))
- (λi,p.s (S (i + (n - S nindex)+nindex))))
- nindex2));
- napply lt_canc;
- nrewrite > (ad_hoc2 … L); nwhd in ⊢ (?(?%?)?);
- nrewrite > (ad_hoc3 … L);
- napply (eq_rect_CProp0_r ?? (λx.λ_.x < ?) ?? (assoc …));
- napply lt_canc; nnormalize in ⊢ (?%?); nwhd in ⊢ (??%);
- napply lt_to_lt_plus; nassumption
- ##|##2: #i; #_; nrewrite > (S_plus i nindex); napply refl]
- ##| napply ad_hoc4]##]
- ##| nwhd in ⊢ (???%?);
- nchange in Hni1 with (nindex < S n);
- ngeneralize in match (le_S_S_to_le … Hni1) in ⊢ ?;
- nwhd in ⊢ (? → ???(???????%?)?);
- napply (nat_rect_CProp0
- (λx. nindex ≤ x →
- eq_rel (carr A) (eq A)
- (partition_splits_card_map A P (S n) s f fi
- (plus
- (big_plus (minus x nindex) (λi.λ_:i < minus x nindex.s (S (plus i nindex))))
- nindex2) x) y) ?? n)
- [ #K; nrewrite < (minus_O_n nindex); nwhd in ⊢ (???(???????%?)?);
- nwhd in ⊢ (???%?); nchange in Hni21 with (nindex2 < s nindex);
- ngeneralize in match (le_O_to_eq … K) in ⊢ ?; #K';
- ngeneralize in match Hni21 in ⊢ ?;
- ngeneralize in match Hni22 in ⊢ ?;
- nrewrite > K' in ⊢ (% → % → ?); #K1; #K2;
- nrewrite > (ltb_t … K2);
- nwhd in ⊢ (???%?); nassumption
- | #n'; #Hrec; #HH; nelim (le_to_lt_or_eq … HH)
- [##2: #K; nrewrite < K; nrewrite < (minus_canc nindex);
- nwhd in ⊢ (???(???????%?)?);
- nrewrite > K;
- nwhd in ⊢ (???%?); nrewrite < K; nrewrite > (ltb_t … Hni21);
- nwhd in ⊢ (???%?); nassumption
- ##| #K; ngeneralize in match (le_S_S_to_le … K) in ⊢ ?; #K';
- nwhd in ⊢ (???%?);
- ngeneralize in match (?:
- ¬ (big_plus (S n' - nindex) (λi,p.s (S (i+nindex))) + nindex2 < s (S n'))) in ⊢ ?
- [ #N; nrewrite > (ltb_f … N); nwhd in ⊢ (???%?);
- ngeneralize in match (Hrec K') in ⊢ ?; #Hrec';
- napply (eq_rect_CProp0_r ??
- (λx,p. eq_rel (carr A) (eq A) (partition_splits_card_map A P (S n) s f fi
- (big_plus x ? + ? - ?) n') y) ?? (minus_S n' nindex K'));
- nrewrite > (split_big_plus (S (n' - nindex)) (n' - nindex)
- (λi,p.s (S (i+nindex))) (le_S ?? (le_n ?)));
- nrewrite > (ad_hoc5 (n' - nindex));
- nnormalize in ⊢ (???(???????(?(?(??%)?)?)?)?);
- nrewrite > (ad_hoc6 … K');
- nrewrite > (ad_hoc7 (big_plus (n' - nindex) (λi,p.s (S (i+nindex))))
- (s (S n')) nindex2);
- nassumption
- | nrewrite > (minus_S … K');
- nrewrite > (split_big_plus (S (n' - nindex)) (n' - nindex)
- (λi,p.s (S (i+nindex))) (le_S ?? (le_n ?)));
- nrewrite > (ad_hoc5 (n' - nindex));
- nnormalize in ⊢ (?(?(?(??%)?)?));
- nrewrite > (ad_hoc6 … K');
- napply ad_hoc8]##]##]##]
-##| #x; #x'; nnormalize in ⊢ (? → ? → %);
- nelim daemon
- ]
+ @ xxx; @
+ [ napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption ]
+ ##| nwhd in ⊢ (???%%); napply (.= ?) [##3: nassumption|##skip]
+ nlapply (iso_nat_nat_union_char n s xxx ?)
+ [napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##]
+ *; *; #K1; #K2; #K3;
+ nlapply
+ (iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n))
+ nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????); /2/
+ [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; //
+ | nassumption ]##]
+##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
+ ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2');
+ ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
+ nlapply(disjoint … P (f i1) (f i1') ???)
+ [##2,3: napply f_closed; //
+ |##1: @ (fi i1 i2); @;
+ ##[ napply f_closed; // ##| alias symbol "refl" = "refl1".
+napply (. E‡#);
+ nwhd; napply f_closed; //]##]
+ #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); // ##]
+ #E''; nrewrite < E''; @; //;
+ nrewrite < E'' in E; #E'''; napply (f_inj … E'''); //;
+ nrewrite > E''; // ]##]
+ ##] #K;
+ nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x;
+ nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x';
+ nlapply (K … E)
+ [##1,2: nassumption;
+ ##|##3,4:napply le_to_le_S_S; nassumption; ##]
+ *; #K1; #K2;
+ napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x');
+ napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x);
+ nrewrite > K1; nrewrite > K2; napply refl.