proposition: Lemma dsum_is_coproduct (P : {fpmod R}) (i1 : 'Mor(M,P)) (i2 : 'Mor(N,P)) : exists phi : 'Mor(dsum,P), i1 = inj1 ** phi /\ i2 = inj2 ** phi.
proof: Proof. exists (proj1 ** i1 + proj2 ** i2). rewrite !mulmorDr !mulmorA inj1_proj1 inj1_proj2 inj2_proj1 inj2_proj2. by rewrite !mul1mor !mul0mor addr0 add0r. 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