proposition: Lemma partn_biggcd (I : finType) (P : pred I) F pi : #|SimplPred P| > 0 -> (forall i, P i -> F i > 0) -> (\big[gcdn/0]_(i | P i) F i)`_pi = \big[gcdn/0]_(i | P i) (F i)`_pi.
proof: Proof. move=> ntP F_gt0; set d := \big[gcdn/0]_(i | P i) F i. have d_gt0: 0 < d. case/card_gt0P: ntP => i /= Pi; have:= F_gt0 i Pi. rewrite !lt0n -!dvd0n; apply: contra => dv0d. by rewrite (dvdn_trans dv0d) // (@biggcdn_inf _ i). apply/eqP; rewrite eqn_dvd; apply/andP; split. by apply/dvdn_biggcdP=> i Pi; rewrite partn_dvd ?F_gt0 // (@biggcdn_inf _ i). rewrite -(dvdn_pmul2r (part_gt0 pi^' d)) partnC //. apply/dvdn_biggcdP=> i Pi; rewrite -(partnC pi (F_gt0 i Pi)) dvdn_mul //. by rewrite (@biggcdn_inf _ i). by rewrite partn_dvd ?F_gt0 // (@biggcdn_inf _ i). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)