op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i))
\big[op,nil]_{i ∈ [a,b[ |p i}(f i).
#a #b # c #p #B #nil #op #f #leab #lebc
op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i))
\big[op,nil]_{i ∈ [a,b[ |p i}(f i).
#a #b # c #p #B #nil #op #f #leab #lebc
>minus_plus >(commutative_plus a) <plus_minus_m_m //
>bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
[#i #lei >plus_minus // <plus_minus1
>minus_plus >(commutative_plus a) <plus_minus_m_m //
>bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
[#i #lei >plus_minus // <plus_minus1
#n #Hind cases(true_or_false (p1 n)) #Hp1
[>bigop_Strue // >Hind >bigop_sum @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
#n #Hind cases(true_or_false (p1 n)) #Hp1
[>bigop_Strue // >Hind >bigop_sum @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
>div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
|>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
>div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
|>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
#k #p #B #nil #op #f #g (elim k) [normalize @nill]
-k #k #Hind (cases (true_or_false (p k))) #H
[>bigop_Strue // >bigop_Strue // >bigop_Strue //
#k #p #B #nil #op #f #g (elim k) [normalize @nill]
-k #k #Hind (cases (true_or_false (p k))) #H
[>bigop_Strue // >bigop_Strue // >bigop_Strue //
iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
\big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
#n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
\big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
#n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
[(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
>bigop_Sfalse
[@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
[(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
>bigop_Sfalse
[@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
|#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) *
#ltkj #p1kj #eqj % // % //
(cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
|#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) *
#ltkj #p1kj #eqj % // % //
(cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //