proposition: Lemma mxOver_constE c S : (m > 0)%N -> (n > 0)%N -> (const_mx c \is a mxOver S) = (c \in S).
proof: Proof. move=> m_gt0 n_gt0; apply/idP/idP; last exact: mxOver_const. by move=> /mxOverP /(_ (Ordinal m_gt0) (Ordinal n_gt0)); rewrite mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)