proposition: Lemma big_dvdr_gcdr (I : finType) (F : I -> R) : forall i, \big[(@gcdr R)/0]_i F i %| F i.
proof: Proof. move=> i; elim: (index_enum I) (mem_index_enum i)=> // a l IHl. rewrite in_cons big_cons =>/orP [/eqP ->|H]. by rewrite dvdr_gcdl. exact: (dvdr_trans (dvdr_gcdr _ _) (IHl H)). 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