∀ f n p, O < p ⇒ (bigop n (λi. true) 1 times (λi. f i)) ≡ (bigop n (λi. true) 1 times (λi. mod (f i) p)) [p]

Theorem congruent_pi : forall (f:(nat.nat -> nat.nat)), forall (n:nat.nat), forall (p:nat.nat), (nat.lt nat.O p) -> cong.congruent (bigops.bigop (nat.nat) n (fun (i:nat.nat) => bool.true) (nat.S nat.O) nat.times (fun (i:nat.nat) => f i)) (bigops.bigop (nat.nat) n (fun (i:nat.nat) => bool.true) (nat.S nat.O) nat.times (fun (i:nat.nat) => div_mod.mod (f i) p)) p.

theorem congruent_pi : \forall (f:nat -> nat). \forall (n:nat). \forall (p:nat). ((lt) (O) p) -> (congruent) ((bigop) (nat) n (\lambda i : nat. (true) ) ((S) (O) ) (times) (\lambda i : nat. f i)) ((bigop) (nat) n (\lambda i : nat. (true) ) ((S) (O) ) (times) (\lambda i : nat. (mod) (f i) p)) p.

theorem congruent_pi : forall (f:(nat.nat) -> nat.nat) , forall (n:nat.nat) , forall (p:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> ((((cong.congruent) ) (((((((bigops.bigop) (nat.nat)) (n)) (fun (i : nat.nat) , (bool.true) )) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (f) (i)))) (((((((bigops.bigop) (nat.nat)) (n)) (fun (i : nat.nat) , (bool.true) )) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (((div_mod.mod) ) ((f) (i))) (p)))) (p).

congruent_pi : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(p:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(p) => cong_sttfa_th.congruent(bigops_sttfa_th.bigop[nat_sttfa_th.sttfa_nat](n)((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.sttfa_true))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(i))))(bigops_sttfa_th.bigop[nat_sttfa_th.sttfa_nat](n)((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.sttfa_true))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):div_mod_sttfa_th.mod(f(i))(p))))(p)))))

Printing for OpenTheory is not working at the moment.