proposition: Lemma bareiss_recE : forall m a (M: 'M[R]_(1 + m)), lreg a -> (forall (k:nat) (f1 f2: 'I_k.+1 -> 'I_m.+1), a ^+ k %| minor f1 f2 M) -> (forall p (h h' :p.+1 <= 1 + m), lreg (minor (widen_ord h) (widen_ord h') M)) -> a ^+ m * (bareiss_rec a M) = \det M.
proof: Proof. elim => [ | m hi] //=. - move => a M ha h1 h2. by rewrite expr0 {2}[M]mx11_scalar det_scalar1 mul1r. rewrite [(1 + m.+1)%nat]/(1 + (1 + m))%nat => a M ha. set d := M 0 0. set l := ursubmx M. set c := dlsubmx M. set N := drsubmx M. have heq : block_mx (M 0 0)%:M (ursubmx M) (dlsubmx M) (drsubmx M) = M. - have -> : (M 0 0)%:M = ulsubmx M by apply/matrixP => i j; rewrite !mxE [i]ord1 [j]ord1 {i j} !lshift0. by rewrite submxK. rewrite -{1 2}heq => hM hm. have : forall p (h h': p.+1 <= 1 + (1 + m)), lreg (minor (widen_ord h) (widen_ord h') M). - rewrite -heq => p h h'. rewrite (@minor_eq _ _ _ _ _ (widen_ord h) _ (widen_ord h)) ?hm//. by move => x; apply/ord_inj. case: (@sketch _ _ a (M 0 0) (ursubmx M) (dlsubmx M) (drsubmx M) ha hM hm) => hM00 h1 h2 h3 hlreg. have h3' : forall p (h h': p < 1 + m), lreg (pminor h h' (dvd_step a (d *: N - c *m l))) by move => p h h'; apply/h3. move: (hi d (dvd_step a (d *: N - c *m l)) hM00 h1 h3'). set r := bareiss_rec _ _ => hh. have : a ^+ m.+1 *( d ^+m * r) = a ^+ m.+1 * \det (dvd_step a (d *: N - c *m l)) by rewrite hh. rewrite det_dvd_step //; last by move => i j; apply (det_dvd_step_tool h2). move => heq2. have hX : lreg (M 0 0 ^+ (1 + m)) by apply/lregX. apply/hX. rewrite -{3}heq bareiss_key_lemma -heq2 [M 0 0 ^+ (1 + m)]exprS -mulrA. congr(_ * _). by rewrite mulrCA. 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