proposition: Fact mxOver_add_subproof : addr_closed (@mxOver m n _ addS).
proof: Proof. split=> [|p q Sp Sq]; first by rewrite mxOver0 // ?rpred0. by apply/mxOverP=> i j; rewrite mxE rpredD // !(mxOverP _). 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)