proposition: Lemma lift_epi (M N L : {fpmod R}) (phi : 'Mor(M,N)) (psi : 'Epi(N,L)) : phi ** psi %= 0 -> is_epi (lift phi psi).
proof: Proof. move=> /mul_lift psiP K kapa; rewrite eqmor_sym in psiP. suff lepi : is_epi (lift phi psi) by move/lepi. apply: right_epi (coker phi) _ _. exact: (@eqmor_epi _ _ _ psi). 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