∀ a b p f, a ≤ b ⇒ (bigop (b - a) (λi. p (i + a)) 1 times (λi. f (i + a))) = (bigop b (λi. andb (leb a i) (p i)) 1 times (λi. f i))

Theorem bigop_I_gen : forall (a:nat.nat), forall (b:nat.nat), forall (p:(nat.nat -> bool.bool)), forall (f:(nat.nat -> nat.nat)), (nat.le a b) -> logic.eq (nat.nat) (bigop (nat.nat) (nat.minus b a) (fun (i:nat.nat) => p (nat.plus i a)) (nat.S nat.O) nat.times (fun (i:nat.nat) => f (nat.plus i a))) (bigop (nat.nat) b (fun (i:nat.nat) => bool.andb (nat.leb a i) (p i)) (nat.S nat.O) nat.times (fun (i:nat.nat) => f i)).

theorem bigop_I_gen : \forall (a:nat). \forall (b:nat). \forall (p:nat -> bool). \forall (f:nat -> nat). ((le) a b) -> (eq) (nat) ((bigop) (nat) ((minus) b a) (\lambda i : nat. p ((plus) i a)) ((S) (O) ) (times) (\lambda i : nat. f ((plus) i a))) ((bigop) (nat) b (\lambda i : nat. (andb) ((leb) a i) (p i)) ((S) (O) ) (times) (\lambda i : nat. f i)).

theorem bigop_I_gen : forall (a:nat.nat) , forall (b:nat.nat) , forall (p:(nat.nat) -> bool.bool) , forall (f:(nat.nat) -> nat.nat) , ((((nat.le_) ) (a)) (b)) -> (((logic.eq_) (nat.nat)) (((((((bigops.bigop) (nat.nat)) ((((nat.minus) ) (b)) (a))) (fun (i : nat.nat) , (p) ((((nat.plus) ) (i)) (a)))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (f) ((((nat.plus) ) (i)) (a))))) (((((((bigops.bigop) (nat.nat)) (b)) (fun (i : nat.nat) , (((bool.andb) ) ((((nat.leb) ) (a)) (i))) ((p) (i)))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (f) (i))).

bigop_I_gen : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):(FORALL(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(nat_sttfa_th.le(a)(b) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(b)(a))((LAMBDA(i:nat_sttfa_th.sttfa_nat):p(nat_sttfa_th.plus(i)(a))))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(nat_sttfa_th.plus(i)(a)))))(bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](b)((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.andb(nat_sttfa_th.leb(a)(i))(p(i))))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(i)))))))))

Printing for OpenTheory is not working at the moment.