proposition: Lemma bareiss_recE : forall m a (M : 'M[{poly R}]_(1 + m)), a \is monic -> (forall p (h h' : p < 1 + m), pminor h h' M \is monic) -> (forall k (f g : 'I_k.+1 -> 'I_m.+1), rdvdp (a ^+ k) (minor f g M)) -> a ^+ m * (bareiss_rec a M) = \det M.
proof: Proof. elim=> [a M _ _ _|m ih a M am hpm hdvd] /=. by rewrite expr0 mul1r {2}[M]mx11_scalar det_scalar1. have ak_monic k : a ^+ k \is monic by apply/monic_exp. set d := M 0 0; set M' := (_ - _); set M'' := map_mx _ _; rewrite /= in M' M'' *. have d_monic : d \is monic. have -> // : d = pminor (ltn0Sn _) (ltn0Sn _) M. have h : widen_ord (ltn0Sn m.+1) =1 (fun=> 0) by move=> x; apply/ord_inj; rewrite [x]ord1. by rewrite /pminor (minor_eq h h) minor1. have dk_monic : forall k, d ^+ k \is monic by move=> k; apply/monic_exp. have hM' : M' = a *: M''. pose f := fun m (i : 'I_m) (x : 'I_2) => if x == 0 then 0 else lift 0 i. apply/matrixP => i j. rewrite !mxE big_ord1 !rshift1 [a * _]mulrC rdivpK ?(eqP am,expr1n,mulr1) //. move: (hdvd 1%nat (f _ i) (f _ j)). by rewrite !minor2 /f /= expr1 !mxE !lshift0 !rshift1. rewrite -[M]submxK; apply/(@lregX _ d m.+1 (monic_lreg d_monic)). have -> : matrix.ulsubmx M = d%:M by apply/rowP=> i; rewrite !mxE ord1 lshift0. rewrite bareiss_key_lemma -/M' hM' detZ mulrCA [_ * (a ^+ _ * _)]mulrCA !exprS -!mulrA. rewrite ih // => [p h h'|k f g]. rewrite -(@monicMl _ (a ^+ p.+1)) // -detZ -submatrix_scale -hM'. rewrite -(monicMl _ d_monic) bareiss_block_key_lemma_sub monicMr //. by rewrite (minor_eq (lift_pred_widen_ord h) (lift_pred_widen_ord h')) hpm. case/rdvdpP: (hdvd _ (lift_pred f) (lift_pred g)) => // x hx. apply/rdvdpP => //; exists x. apply/(@lregX _ _ k.+1 (monic_lreg am))/(monic_lreg d_monic). rewrite -detZ -submatrix_scale -hM' bareiss_block_key_lemma_sub. by rewrite mulrA [x * _]mulrC mulrACA -exprS [_ * x]mulrC -hx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(ssrcomplements minor dvdring) polydvd