proposition: Lemma big_gcdrP (I : finType) (F : I -> R) d : (forall i, d %| F i) -> d %| \big[(@gcdr R)/0]_(i : I) F i.
proof: Proof. move=> Hd ; elim: (index_enum I)=> [|a l IHl]. by rewrite big_nil dvdr0. rewrite big_cons dvdr_gcd. by apply/andP; split; [apply: Hd | apply: IHl]. 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