- m (H1: lt m (big_plus ? s)) index (p: lt index (card ? P)) on index : A ≝
- match index return λx. lt x (card ? P) → ? with
- [ O ⇒ λp'.f ??? (H O p') m ?
- | S index' ⇒ λp'.
- match ltb m (s index p) with
- [ or_introl K ⇒ f ??? (H index p) m K
- | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s index p)) ? index' ? ]] p.
-##[##2: napply lt_minus; nassumption
- |##3: napply lt_Sn_m; nassumption
- |
+ m index on index:
+ le (S index) (card ? P) → lt m (big_plus (S index) (λi,p. s i ?)) → lt index (card ? P) → A ≝
+ match index return λx. le (S x) (card ? P) → lt m (big_plus (S x) ?) → lt x (card ? P) → ? with
+ [ O ⇒ λL,H1,p.f ??? (H O p) m ?
+ | S index' ⇒ λL,H1,p.
+ match ltb m (s (S index') p) with
+ [ or_introl K ⇒ f ??? (H (S index') p) m K
+ | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s (S index') p)) index' ??? ]].
+##[##3: napply lt_minus; nelim daemon (*nassumption*)
+ |##4: napply lt_Sn_m; nassumption
+ |##5: napply (lt_le_trans … p); nassumption
+##|##2: napply lt_to_le; nassumption
+##|##1: nnormalize in H1; nelim daemon ]