fact: Definition mxundef T (x : mtx T) : mtx2 := match x with | nown => nown | mx None => own | _ => undef end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)