proposition: Lemma Gaussian_elimination_map m n (A : 'M_(m, n)) : Gaussian_elimination_ A^f = ((col_ebase A)^f, (row_ebase A)^f, \rank A).
proof: Proof. rewrite mxrankE /row_ebase /col_ebase unlock. elim: m n A => [|m IHm] [|n] A /=; rewrite ?map_mx1 //. set pAnz := [pred k | A k.1 k.2 != 0]. rewrite (@eq_pick _ _ pAnz) => [|k]; last by rewrite /= mxE fmorph_eq0. case: {+}(pick _) => [[i j]|]; last by rewrite !map_mx1. rewrite mxE -fmorphV -map_xcol -map_xrow -map_dlsubmx -map_drsubmx. rewrite -map_ursubmx -map_mxZ -map_mxM -map_mxB {}IHm /=. case: {+}(Gaussian_elimination_ _) => [[L U] r] /=; rewrite map_xrow map_xcol. by rewrite !(@map_block_mx _ _ f 1 _ 1) !map_mx0 ?map_mx1 ?map_scalar_mx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)