proposition: Lemma inj1_proof : pres dsum %| pres M *m (row_mx 1%:M 0).
proof: Proof. apply/dvdmxP; exists (row_mx 1%:M 0). by rewrite mul_mx_row mul_row_block !(mulmx0, mul0mx) !addr0 mul1mx mulmx1. 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