proposition: Lemma morph_prod I r (P : pred I) F : (forall i, P i -> F i \in D) -> f (\prod_(i <- r | P i) F i) = \prod_( i <- r | P i) f (F i).
proof: Proof. move=> D_F; elim/(big_load (fun x => x \in D)): _. elim/big_rec2: _ => [|i _ x Pi [Dx <-]]; first by rewrite morph1. by rewrite groupM ?morphM // D_F. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)