+
+theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤b →
+\big[op,nil]_{i∈[a,b[ |p i}(f i) = \big[op,nil]_{i < b|leb a i ∧ p i}(f i).
+#a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
+cut (∀a,b. a ≤ b → S b - a = S (b -a))
+ [#a #b cases a // #a1 #lta1 normalize >eq_minus_S_pred >S_pred
+ /2 by lt_plus_to_minus_r/] #Hcut
+cases (le_to_or_lt_eq … lea) #Ha
+ [cases (true_or_false (p b)) #Hcase
+ [>bigop_Strue [2: >Hcase >(le_to_leb_true a b) // @le_S_S_to_le @Ha]
+ >(Hcut … (le_S_S_to_le … Ha))
+ >bigop_Strue
+ [@eq_f2
+ [@eq_f <plus_minus_m_m [//|@le_S_S_to_le //] @Hind
+ |@Hind @le_S_S_to_le //
+ ]
+ |<plus_minus_m_m // @le_S_S_to_le //
+ ]
+ |>bigop_Sfalse [2: >Hcase cases (leb a b)//]
+ >(Hcut … (le_S_S_to_le … Ha)) >bigop_Sfalse
+ [@Hind @le_S_S_to_le // | <plus_minus_m_m // @le_S_S_to_le //]
+ ]
+ |<Ha <minus_n_n whd in ⊢ (??%?); <(bigop_false a B nil op f) in ⊢ (??%?);
+ @same_bigop // #i #ltia >(not_le_to_leb_false a i) // @lt_to_not_le //
+ ]
+qed.
+