proposition: Lemma L3 m (d: R) (l: 'rV[R]_m) (c c0: 'cV[R]_m) (M: 'M[R]_m): \det (block_mx d%:M l c M) = \det (block_mx d%:M l (c - d *: c0) (M - c0 *m l)).
proof: Proof. pose X := block_mx d%:M l c M. have huniq : uniq (map (lift 0) (enum 'I_m)). - rewrite map_inj_in_uniq ?enum_uniq //. move => i j hi hj /=. by apply/lift_inj. have htool : forall s, 0 \notin map (lift 0) s by move => n /=; elim. have {}htool := htool _ (enum 'I_m). have -> : block_mx d%:M l (c -d *: c0) (M - c0 *m l) = foldl (fun N i => line_comb i 0 (-(L3tool c0 d i)) N) X (map (lift 0) (enum 'I_m)). - apply/row_matrixP => i. case: (lines_comb_row_dep (fun i => - (L3tool c0 d i)) X huniq htool) => hl hr. move: (hl i) (hr i) => {hl hr}. case: (splitP i) => j. + rewrite [j]ord1 {j} => hi. have {hi i}-> : i = 0 by apply/ord_inj. move => _ -> //=. apply/rowP => j; rewrite !mxE. by case: splitP. move => hi. have {i hi}-> : i = lift 0 j by apply/ord_inj. move => -> /=. + rewrite L3toolES => _. apply/rowP => k; rewrite !mxE. case: splitP => x /= ; first by rewrite [x]ord1. rewrite /bump leq0n => /eqP; rewrite eqSS => /eqP/ord_inj{j}->. case: splitP => z //; rewrite [z]ord1 {z} !mxE => _. case: splitP => y; rewrite !mxE. * rewrite [y]ord1 {y} => _. by rewrite mulrC mulr1n mulNr. by move => _; rewrite big_ord_recl big_ord0 addr0 mulNr. rewrite mem_map ?mem_enum //. by apply/lift_inj. by rewrite det_lines_comb_dep // size_map size_enum_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