proposition: Lemma big_gcdr_def (I : finType) (F : I -> R) d : (exists k, F k %| d) -> \big[(@gcdr R)/0]_(i : I) F i %| d.
proof: Proof. by case=> k; apply: dvdr_trans; apply: big_dvdr_gcdr. 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