fact: Variables (All : matrix R m2 n1) (Alr : matrix R m2 n2).
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms