proposition: Lemma sketch m n (a d: R) (l: 'rV[R]_n) (c: 'cV[R]_m) (M: 'M[R]_(m,n)): lreg a -> (forall (k:nat) (f1: 'I_k.+1 -> 'I_(1 + m)) (f2: 'I_k.+1 -> 'I_(1 + n)), a ^+ k %| minor f1 f2 (block_mx d%:M l c M))-> (forall p (h: p.+1 <= 1 + m) (h': p.+1 <= 1 + n), lreg (pminor h h' (block_mx d%:M l c M))) -> let M' := d *: M - c *m l in let M'':= dvd_step a M' in [/\ lreg d, (forall k (f1: 'I_k.+1 -> 'I_m) (f2: 'I_k.+1 -> 'I_n), d ^+ k %| minor f1 f2 M''), M' = a *: M'' & (forall p (h: p.+1 <= m) (h': p.+1 <= n), lreg (pminor h h' M''))].
proof: Proof. rewrite /pminor => ha hM hN. set M0 := block_mx d%:M l c M. have hh : d = minor (widen_ord (ltn0Sn _)) (widen_ord (ltn0Sn _)) M0. - rewrite (@minor_eq _ _ _ _ _ (fun=> 0) _ (fun=> 0)) ?minor1 //. + by rewrite /M0 blockE00. + by move => x; rewrite ord1; apply: val_inj. + by move => x; rewrite ord1; apply: val_inj. have h2 : lreg d. - by rewrite hh /M0; apply hN. set M' := d *: M - c *m l. set M'' := dvd_step a M'. set f : forall m, 'I_m -> 'I_2 -> 'I_(1 + m) := fun m (i: 'I_m) (x: 'I_2) => if x == 0 then 0 else lift 0 i. have h4 : forall i j, a %| M' i j. - move => i j; rewrite /M' !mxE big_ord_recl big_ord0 addr0. move: (hM 1%nat (f _ i) (f _ j)). by rewrite !minor2 /f /= expr1 blockE00 blockEi0 blockE0i blockEij. have h6 : forall i j, M' i j = a * M'' i j. - move => i j; rewrite [(dvd_step _ _) i j]mxE. case: odivrP => [dv|h] /=; first by rewrite mulrC. case/dvdrP: (h4 i j) => dv hdv. by move: (h dv); rewrite hdv eqxx. have h6' : M' = a *: M'' by apply/matrixP => i j; rewrite h6 !mxE. have h7 : forall k (f1: 'I_k -> 'I_m) (f2: 'I_k -> 'I_n), minor f1 f2 M' = a ^+ k * minor f1 f2 M''. - move => k f1 f2. by rewrite h6' /minor submatrix_scale detZ. have h8: forall k (f1: 'I_k -> 'I_m) (f2: 'I_k -> 'I_n), d * minor f1 f2 M' = d ^+ k * minor (lift_pred f1) (lift_pred f2) M0. - move => k f1 f2. by rewrite /M0 /M' key_lemma_sub. have ak : forall k, lreg (a^+k). - by move => k; apply/lregX. have h10 : forall k (f1: 'I_k.+1 -> 'I_m) (f2: 'I_k.+1 -> 'I_n), d ^+ k %| minor f1 f2 M''. - move => k f1 f2. move/lregP : (ak k.+1) => ak'. rewrite -(@dvdr_mul2l _ (a^+k.+1)) // -h7. have hM0 : d != 0 by apply/lregP. have hMk : d^+ k.+1 != 0 by apply/lregP/lregX. rewrite -(@dvdr_mul2l _ d) // mulrA h8 //. by rewrite mulrAC -exprS dvdr_mul2l //. split => //. rewrite -/M'' => p h h'. apply/(@lregMl _ (a ^+ p.+1)). rewrite -h7. apply/(@lregMl _ d). rewrite h8. apply/lregM; first by apply/lregX. rewrite (@minor_eq _ _ _ _ _ (widen_ord (size_tool h)) _ (widen_ord (size_tool h'))) ?hN. - by apply: hN. - by move => x; apply: val_inj; rewrite lift_pred_widen_ord. - by move => x; apply: val_inj; rewrite lift_pred_widen_ord. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly polydiv mxpoly) ssrcomplements dvdring minor atomic_operations