proposition: Lemma homology_dvd : homology_alt_pres %| pres homology.
proof: Proof. rewrite /homology /homology_alt_pres. rewrite dvd_mx_col /= !dvd_ker dvd_quot_mx ?ker_modK //=. rewrite -[X in _ %| X](subrK phi%:m) dvdmxDl ?dvd_col_mxl //=. rewrite (dvdmx_trans (dvd_col_mxu _ _)) //. have := @factorP _ _ _ [Mono of kernel psi] phi. rewrite /eqmor /= subr0 mulmx1; apply. rewrite (dvdmx_trans (dvd_col_mxl _ _)) // dvd_ker. by move: mul_phi_psi; rewrite /eqmor subr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements stronglydiscrete coherent edr