proposition: Lemma smithmxn_recP : forall m n (M : 'M[R]_(1 + (1 + m),1 + (1 + n))), smith_spec M (smithmxn_rec smith2x2 M).
proof: Proof. elim=> [|m ih [|n] A] /=; first exact: smith2xnP. case: smith2xnP=> L0 d R0 h1 h2 h3 h4. constructor; rewrite ?unitmx_tr //; apply/trmx_inj. by rewrite !trmx_mul !trmxK tr_diag_mx_seq mulmxA. set A1 := usubmx A; set A2 := dsubmx A. case: (ih) => P1 x Q1 hP1xQ1 x_sorted hP1 hQ1; rewrite hP1xQ1. set C := col_mx (A1 *m Q1) _; set D := col_mx (row 0 C) (row 1 C). set E := dsubmx (dsubmx C). case: smith2xnP=> P2 y Q2 hP2yQ2 y_sorted hP2 hQ2. set H := col_mx (P2 *m D *m Q2) (E *m Q2) : 'M[R]_(1 + (1 + _),1 + (1 + _)). set y0 := y`_0; set c := dlsubmx H; set c' := map_mx _ _; set H' := drsubmx H. case: ih=> L1 d R1; rewrite -mulmxA=> hLdR d_sorted hL1 hR1. have dvd_y0_x0 : y0 %| x`_0. have -> : x`_0 = D (rshift 1 0) 0. rewrite col_mxEd !mxE split1. by case: unliftP=> // [[[]]] //= i _; rewrite !mxE. move/(canRL (mulmxK hQ2))/(canRL (mulKmx hP2)): hP2yQ2=> ->. 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 : x`_0 %| x`_i *+ (i == j). by case: (i == j :> nat); rewrite ?sorted_nth0 // mulr0n dvdr0. have Hdvd i j : y0 %| H i j. rewrite -[(1 + (1 + _))%N]/(2 + _)%N; apply: dvdr_col_mx; split=> {}i {}j. rewrite hP2yQ2 !mxE. by case: (i == j :> nat); rewrite ?sorted_nth0 // mulr0n dvdr0. apply: dvdr_mulmxr=> {}i {}j; rewrite /E col_mxKd. apply: dvdr_dsubmx=> {}i {}j; rewrite !mxE. move: (dvdr_trans dvd_y0_x0 (hx0 i j)). by case: (i == j :> nat); rewrite ?(mulr0n,dvdr0,mulr1n). constructor; last first. - by rewrite !unitmx_mul hQ1 hQ2 unitmxE det_lblock det1 mul1r -unitmxE. - rewrite !unitmx_mul /lift0_mx ?(unitmxE,det_lblock,@det_lblock _ 2,det1,mul1r). by rewrite mulr1 -!unitmxE hL1 hP1 hP2. - apply: sorted_cons=> //. move/matrixP: hLdR => /(_ 0 0); rewrite [RHS]mxE mulr1n => <-. exact: (dvdr_mulmxl L1 (dvdr_mulmxr R1 (dvdr_drsubmx Hdvd))). rewrite -[A]vsubmxK -!mulmxA [_ *m (col_mx A1 _ *m _)]mulmxA mul_block_col. rewrite !mul0mx addr0 add0r mul1mx [_ *m (Q1 *m _)]mulmxA [_ *m Q1]mul_col_mx. rewrite hP1xQ1 [_ *m (C *m _)]mulmxA [_ *m (Q2 *m _)]mulmxA diag_mx_seq_cons. have -> : block_mx P2 0 0 1%:M *m C *m Q2 = block_mx y0%:M 0 c H'. rewrite [C]surgery mul_block_col ?simplmx mul_col_mx -/H -[H]submxK. f_equal; apply/rowP=> i; rewrite !mxE hP2yQ2; by case: splitP=> // j hj; rewrite !mxE -hj. rewrite !mulmx_block ?simplmx -hLdR; congr block_mx. rewrite -mulmxA mulNmx -mulmxN -mulmxDr mul_mx_scalar. suff -> : - (y0 *: c') + c = 0 by rewrite mulmx0. apply/colP=> i; rewrite 4!mxE. case: odivrP=> /= [w ->|]; first by rewrite mulrC addrC subrr mxE. move: (Hdvd (rshift 1 i) (lshift _ 0)); rewrite -[H]submxK block_mxEdl. by case/dvdrP=> w hw /(_ w); rewrite hw eqxx. 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