proposition: Lemma eqd_big_mul1 n (P : pred 'I_n) (F : 'I_n -> R) : \prod_(i < n | P i) F i %= 1 -> (forall i, P i -> F i %= 1).
proof: Proof. case: n P F=> [ ? ? ? []|n P F Hb i Hi] //. rewrite (bigD1 i) //= -unitd1 unitrM unitd1 in Hb. by case/andP: Hb. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete