proposition: Lemma dsum_is_product (P : {fpmod R}) (p1 : 'Mor(P,M)) (p2 : 'Mor(P,N)) : exists phi : 'Mor(P,dsum), p1 = phi ** proj1 /\ p2 = phi ** proj2.
proof: Proof. exists (p1 ** inj1 + p2 ** inj2). rewrite !mulmorDl -!mulmorA inj1_proj1 inj1_proj2 inj2_proj1 inj2_proj2. by rewrite !mulmor1 !mulmor0 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