proposition: Lemma eqd_seq_gcdr : \prod_(i < k) s`_i %= \big[(@gcdr [the gcdDomainType of R : Type])/0]_(f : {ffun 'I_k -> 'I_m}) (\big[(@gcdr [the gcdDomainType of R : Type])/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. 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)) => [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)) => [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 Hcfg: (codom f1 \subset codom g1); last first. move/negbT: Hcfg=> /subsetPn [x] /codomP [y Hy] /negP Habs. rewrite /minor (expand_det_row _ y). rewrite [\sum_(_ <_) _](big1 _ xpredT) ?dvdr0 //. move=> j _; rewrite !mxE. have ->: (g j = g1 j :> nat) by []. have ->: (f y = f1 y :> nat) by []. have ->: (f1 y == g1 j :> nat) = false. by apply/negbTE/eqP=> /ord_inj=> H; apply: Habs; rewrite Hy H codom_f. by rewrite mul0r. move/subsetP: Hcfg=> 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]. 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_(_ < _) _. have:= (IHj _ Hi). have ->: C = \prod_i s`_(finfun f i). by apply: eq_bigr=> i _; rewrite ffunE. by apply. move: (sorted_nth0 (sorted_drop j Hs) (g (p ord_max) - j)). rewrite !nth_drop addn0 subnKC //= tpermR; case/orP: (leq_total j (g l))=> //. rewrite leq_eqVlt => /orP [|Hgm]; first by move/eqP=> ->; rewrite leqnn. have Habs: forall i, g i < j. 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|. by rewrite -(card_codom Hf); exact: max_card. by rewrite !card_ord ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent