+nlemma partition_splits_card_output:
+ ∀A. ∀P:partition A. ∀n,s.
+ ∀f:isomorphism ?? (Nat_ (S n)) (indexes ? P).
+ ∀fi:∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i)).
+ ∀x. x ∈ Nat_ (big_plus (S n) (λi.λ_.s i)) →
+ ∃i1.∃i2. partition_splits_card_map A P (S n) s f fi x n = iso_f ???? (fi i1) i2.
+ #A; #P; #n; #s; #f; #fi;
+ nelim n in ⊢ (? → % → ??(λ_.??(λ_.???(????????%)?)))
+ [ #x; nnormalize in ⊢ (% → ?); nrewrite > (plus_n_O (s O)); nchange in ⊢ (% → ?) with (x < s O);
+ #H; napply (ex_intro … O); napply (ex_intro … x); nwhd in ⊢ (???%?);
+ nrewrite > (ltb_t … H); nwhd in ⊢ (???%?); napply refl
+ | #n'; #Hrec; #x; #Hx; nwhd in ⊢ (??(λ_.??(λ_.???%?))); nwhd in Hx; nwhd in Hx: (??%);
+ nelim (ltb_cases x (s (S n'))); *; #K1; #K2; nrewrite > K2; nwhd in ⊢ (??(λ_.??(λ_.???%?)))
+ [ napply (ex_intro … (S n')); napply (ex_intro … x); napply refl
+ | napply (Hrec (x - s (S n')) ?); nwhd; nrewrite < (minus_S x (s (S n')) ?)
+ [ napply ad_hoc9; nassumption | napply not_lt_to_le; nassumption ]##]
+nqed.
+