proposition: Lemma smith2xnP : forall n (M : 'M[R]_(2,1 + (1 + n))), smith_spec M (smith2xn smith2x2 M).
proof: Proof. elim=> [|n ih]; first exact: smith2x2P. rewrite [n.+1]/(1 + n)%N => M /=; set A1 := lsubmx M; set A2 := rsubmx M. case: ih=> /= P1 d1 Q1 h1 h2 hP1 hQ1; set E := rsubmx _. set C := row_mx (P1 *m A1) _ : 'M[R]_(2,1 + (1 + _)); set D := row_mx _ _. case: smith2x2P=> /= P2 d2 Q2 H1 H2 hP2 hQ2. set H := row_mx (P2 *m D *m Q2) _ : 'M[R]_(1 + _, 1 + (1 + _)). case: (smith1xnP _ smith2x2P)=> L1 d R1; rewrite -mulmxA=> hLdR dsorted hL1 hR1. set r := ursubmx H; set r' := map_mx _ _; set H' := drsubmx H : 'rV[R]_(2 + n). have dvd_d20_d0 : d2`_0 %| d1`_0. have -> : d1`_0 = D 0 (rshift 1 0). rewrite row_mxEr !mxE split1 h1; case: unliftP => //= j hj. by rewrite !mxE; case: j hj=> [[]]. move/(canRL (mulmxK hQ2))/(canRL (mulKmx hP2)): H1 => ->. apply: dvdr_mulmxl=> i j; apply: dvdr_mulmxr=> {}i {}j. by rewrite !mxE; case: (i == j :> nat); rewrite ?sorted_nth0 ?mulr0n ?dvdr0. have hx0 i j : d1`_0 %| d1`_i *+ (i == j). by case: eqP => _; rewrite ?sorted_nth0 // mulr0n dvdr0. have Hdvd i j : d2`_0 %| H i j. rewrite -[(1 + (1 + _))%N]/(2 + _)%N /H H1 dvdr_row_mx //; split=> {}i {}j. by rewrite !mxE; case: (i == j :> nat); rewrite ?sorted_nth0 ?mulr0n ?dvdr0. apply: dvdr_mulmxl=> {}i {}j; rewrite /E row_mxKr h1 !mxE. move: (dvdr_trans dvd_d20_d0 (hx0 i (rshift 1 j))). by case: eqP => _; rewrite ?(mulr0n,dvdr0,mulr1n). constructor; rewrite ?unitmx_mul; last first. - rewrite !unitmxE ?(det_lblock,det_ublock,det_lblock Q2,det1,mulr1,mul1r). by rewrite -!unitmxE hQ1 hQ2 hR1. - by rewrite hP2 hP1 unitmxE (@det_ublock _ 1) det1 mul1r -unitmxE hL1. - apply: sorted_cons=> //; move/matrixP: hLdR => /(_ 0 0). rewrite [RHS]mxE mulr1n => <-. exact: (dvdr_mulmxl _ (dvdr_mulmxr _ (dvdr_lsubmx (n0:=2) (dvdr_drsubmx _)))). rewrite -[M]hsubmxK -/A1 -/A2 -[_ *m P1 *m _]mulmxA (mul_mx_row _ A1) -!mulmxA. rewrite [row_mx (P1 *m A1) _ *m (_ *m _)]mulmxA mul_row_block ?simplmx !mulmxA. have -> : lift0_mx L1 *m P2 *m C *m block_mx Q2 0 0 1%:M = lift0_mx L1 *m block_mx d2`_0%:M r 0 H'. rewrite -!mulmxA; congr (_ *m _); rewrite mulmxA [C]surgery2 -mulmxA. rewrite (mul_row_block D) ?simplmx mul_mx_row mulmxA -/H -[H]submxK. f_equal; apply/rowP=> i; rewrite !mxE H1 ?ord1 ?lshift0; by case: splitP=> // j hj; rewrite !mxE -hj. rewrite -[lift0_mx L1 *m _ *m _]mulmxA (mulmx_block d2`_0%:M r) ?simplmx. rewrite mulmx_block ?simplmx mulmxA -mulmxDl mulmxN mul_scalar_mx. have -> : - (d2`_0 *: r') + r = 0. apply/rowP=> i; rewrite 4!mxE. case: odivrP=> /= [w ->|]; first by rewrite mulrC addrC subrr mxE. move: (Hdvd (lshift _ 0) (rshift 1 i)); rewrite -[H]submxK block_mxEur. by case/dvdrP=> w hw /(_ w); rewrite hw eqxx. rewrite mul0mx diag_mx_seq_cons; f_equal; rewrite -[H']hsubmxK mulmxA. rewrite (mul_mx_row _ (lsubmx H')) (mul_row_block (L1 *m lsubmx H')) ?simplmx. rewrite -mulmxA hLdR; apply/rowP=> i; rewrite !mxE. case: splitP=> j ->; rewrite !mxE //= mulr0n big_ord1 !mxE /H' /E row_mxKr h1. case: splitP=> [[[] // []]|] //= [[]] //= m hm hh. by rewrite !mxE big_ord_recl big_ord1 ?(mxE,mulr0n,mulr0,addr0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr