proposition: Lemma isoP : reflect (exists psi, isomorphisms psi) (isom phi).
proof: Proof. rewrite /isom /injm /surjm; apply: (iffP andP) => [[]|[psi]]; last first. by move=> /andP [/rinv_inj -> /linv_surj ->]. rewrite /eqmor !subr0. move=> phi_inj /dvd_col_mxP /sig_eqW [X /= hX]. have Xmor : pres M %| pres N *m X. rewrite (dvdmx_trans phi_inj) // dvd_ker -mulmxA -[X *m _](subrK 1%:M). by rewrite mulmxDr dvdmxDl ?mulmx1 ?dvdmxMl // -dvdmxN opprB. exists (Morphism Xmor); rewrite /isomorphisms andbC /eqmor -dvdmxN opprB hX. rewrite /eqmor (dvdmx_trans phi_inj) // dvd_ker mulmxBl mul1mx. by rewrite -mulmxA -[X in _ - X]mulmx1 -mulmxBr dvdmxMl // -dvdmxN opprB. 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