proposition: Lemma mx2_E11 a b c d : (mx2 a b c d) 1 1 = d.
proof: Proof. have -> : 1 = rshift 1 0 :> 'I_2 by apply/ord_inj. by rewrite block_mxEdr mxE mulr1n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr