proposition: Lemma smith1xnP n (M : 'M[R]_(1,1 + (1 + n))) (smith2xn : 'M[R]_(2,n.+2) -> 'M[R]_2 * seq R * 'M[R]_n.+2) (smith2xnP : forall M, smith_spec M (smith2xn M)) : smith_spec M (smith1xn smith2xn M).
proof: Proof. rewrite /smith1xn; case: smith2xnP; rewrite [2%N]/(1+1)%N=> P d Q h_eq hs hP hQ. have [d0|d_neq0] := (boolP (d`_0 == 0)). constructor; rewrite ?unitmx1 // ?simplmx; apply/matrixP=> i j. move/(canRL (mulmxK hQ))/(canRL (mulKmx hP))/matrixP: h_eq. rewrite diag_mx_seq0; last by rewrite sorted_dvd0r // sorted_cons // dvd0r. rewrite mul0mx mulmx0 ord1 {i} diag_mx_seq_nil. by move/(_ (widen_ord (lt0n 2) 0) j); rewrite !mxE split1; case: unliftP. move/matrixP: h_eq; rewrite -mulmxA [col_mx M 0 *m _]mul_col_mx mul0mx=> h_eq. have hP00 : ((P 0 0)%:M : 'M_1) \in unitmx. rewrite unitmxE det_scalar expr1; apply/unitrPr; exists ((invmx P) 0 0). move/matrixP: (mulVmx hP) => /(_ 0 0); rewrite !mxE !big_ord_recl big_ord0. suff -> : P (lift 0 0) 0 = 0 by rewrite mulr0 !addr0 mulrC. rewrite -{1}[P]submxK (mul_block_col (ulsubmx P)) ?(mulmx0,addr0) in h_eq. move/eqP: (h_eq 1 0) (h_eq 0 0) d_neq0. rewrite ?(mxE,mulr0n,split1); case: unliftP unliftP=> // i _ [] //= _. rewrite ord1 ?(mxE,big_ord_recl,big_ord0) addr0 lshift0 rshift1 mulr1n. by rewrite mulf_eq0; case/orP=> /eqP -> // <-; rewrite mulr0 addr0 eqxx. constructor=> //; apply/matrixP=> i j; rewrite ord1 {i}. move: (h_eq 0 j); rewrite ?(big_ord_recl,big_ord0,addr0,mxE,split1,mulr1n). case: unliftP unliftP => // _ [] //= k _ <-. rewrite ?(ord1,mxE,big_ord_recl,mulr0,addr0,mulrDr,mulrA) {k} big_distrr /=. by do ?congr (_ + _); apply: eq_bigr=> i _; rewrite ?(mxE,big_ord1) mulrA. 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