proposition: Lemma eqd_seq_gcdr : \prod_(i < k) s`_i %= \big[(@gcdr E)/0]_(f : {ffun 'I_k -> 'I_m}) (\big[(@gcdr E)/0]_(g : {ffun 'I_k -> 'I_n}) minor f g (diag_mx_seq m n s)).
proof: Proof. apply/andP; split; last first. rewrite prod_minor_seq; set j := [ffun _ => _]. by apply/(dvdr_trans (big_dvdr_gcdr _ j))/big_dvdr_gcdr. apply: big_gcdrP=> f; apply: big_gcdrP=> g. case: (injectiveb f) /injectiveP=> Hinjf; last first. by rewrite (minor_f_not_injective _ _ Hinjf) dvdr0. case: (injectiveb g) /injectiveP=> Hinjg; last first. by rewrite (minor_g_not_injective _ _ Hinjg) dvdr0. have Hmin k1 i m1 n1 (h : 'I_k1 -> 'I_m1) : (minn m1 n1 <= h i -> n1 <= h i)%N. move=> Hhi; have := (leq_ltn_trans Hhi (ltn_ord (h i))). by rewrite gtn_min ltnn=> /ltnW/minn_idPr <-. case: (altP (@forallP _ (fun i => f i < minn m n)%N))=>[Hwf|]; last first. rewrite negb_forall=> /existsP [x]; rewrite -leqNgt=> /Hmin Hx. by rewrite (minor_eq0l _ _ Hx) dvdr0. case: (altP (@forallP _ (fun i => g i < minn m n)%N))=>[Hwg|]; last first. rewrite negb_forall=> /existsP [x]; rewrite -leqNgt minnC=> /Hmin Hx. by rewrite (minor_eq0r _ _ Hx) dvdr0. pose f1 i := Ordinal (Hwf i). pose g1 i := Ordinal (Hwg i). have Hinjf1 : injective f1. by move=> x y /eqP; rewrite -(inj_eq (@ord_inj _)) /= => /eqP/ord_inj/Hinjf. have Hinjg1 : injective g1. by move=> x y /eqP; rewrite -(inj_eq (@ord_inj _)) /= => /eqP/ord_inj/Hinjg. case/boolP: (codom f1 \subset codom g1); last first. case/subsetPn => x /codomP [y Hy] Habs. rewrite /minor (expand_det_row _ y). rewrite [\sum_(_ <_) _](big1 _ xpredT) ?dvdr0 // => j _. rewrite !mxE -[(g j : nat)]/(g1 j : nat) -[(f y : nat)]/(f1 y : nat). suff /negbTE->: (f1 y != g1 j :> nat) by rewrite mul0r. by apply: contraNneq Habs =>/ord_inj H; rewrite Hy H codom_f. move/subsetP => Hcfg. pose f' i := widen_minl (f1 i). pose g' i := widen_minr (g1 i). have ->: minor f g (diag_mx_seq m n s) = minor f' g' (diag_mx_seq m n s). by apply: minor_eq=> i; apply: ord_inj. rewrite (eqd_dvdr _ (minor_diag_mx_seq Hinjf1 Hinjg1 Hcfg)) //. move: Hinjf1; clear -Hs; move: f1; clear -Hs. elim: k =>[?|j /= IHj g Hg]; first by rewrite big_ord0 dvd1r. rewrite big_ord_recr /=. pose max:= \max_i (g i). have [l Hl]: {j | max = g j} by apply: eq_bigmax; rewrite card_ord. pose p := tperm l ord_max. set B := \prod_(_ < _) _. rewrite (reindex_inj (@perm_inj _ p)) /= big_ord_recr /= dvdr_mul //. pose f := g \o p \o (widen_ord (leqnSn j)). have Hf: injective f. apply: inj_comp=> [|x y /eqP]. by apply: inj_comp=> //; exact: perm_inj. by rewrite -(inj_eq (@ord_inj _)) /= => H; apply/ord_inj/eqP. have Hi: injective (finfun f). by move=> x e; rewrite !ffunE; exact: Hf. set C := \prod_(_ < _) _. suff ->: C = \prod_i s`_(finfun f i) by apply: IHj. by apply: eq_bigr=> i _; rewrite ffunE. have jleg : (j <= g (p ord_max))%N. rewrite /= tpermR; case: ltngtP => // Hgm. have Habs: forall i, (g i < j)%N. move=> i; apply: (leq_ltn_trans _ Hgm). by rewrite -Hl /k; exact: (leq_bigmax i). pose f := fun x => Ordinal (Habs x). have Hf: injective f. move=> x y /eqP; rewrite -(inj_eq (@ord_inj _)) /= => /eqP Hxy. by apply/Hg/ord_inj. have: (#|'I_j.+1| <= #|'I_j|)%N. by rewrite -(card_codom Hf); exact: max_card. by rewrite !card_ord ltnn. have [glts | sleg] := ltnP (g (p ord_max)) (size s); last first. by rewrite (nth_default 0 sleg); exact: dvdr0. apply: sorted_leq_nth=>//; first exact: dvdr_trans. by rewrite inE; apply/leq_ltn_trans/glts. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)