proposition: Lemma sdvd_Bezout_step2 m n i j u' vM (M : 'M[R]_(1 + m, 1 + n)) : let B : 'M_(1 + m, 1 + n) := block_mx (M 0 0)%:M vM (const_mx (M 0 0)) (u' *m vM + drsubmx M) in let C := xrow 0 i B in ~~ (M 0 0 %| B i (lift 0 j)) -> (Bezout_step (C 0 0) (C 0 (lift 0 j)) C^T j)^T 0 0 %<| M 0 0.
proof: Proof. set B := block_mx _ _ _ _ => /=. set C := xrow _ _ _. have ->: M 0 0 = C^T 0 0. rewrite /C /B -(lshift0 n 0) !mxE tpermL. by case: splitP=> [i' _|i' Hi']; rewrite ?ord1 row_mxEl mxE ?eqxx. move=> ndvd. rewrite mxE. rewrite -[C]trmxK [C^T^T^T]trmxK ![C^T^T _ _]mxE sdvd_Bezout_step //. by rewrite {2}/C [_ (lift _ _) _]mxE [matrix.xrow _ _ _ _ _]mxE tpermL. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg ssrint ssrnum fintype choice) mathcomp(matrix mxalgebra bigop zmodp perm) dvdring mxstructure stronglydiscrete coherent edr