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