fact: Definition divid m n (I : 'cV[R]_m) (J : 'cV[R]_n) : 'M_(m, n):= if subidP I J is ReflectT P then projT1 (sig_eqW P) else 0.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice fingroup) mathcomp(matrix bigop zmodp mxalgebra poly) ssrcomplements