proposition: Lemma block_mxEll : forall i j, A (rshift m1 i) (lshift n2 j) === All i j.
proof: Proof. by move=> i j; rewrite /A /block_mx /trmx; rewrite -> pastemxEr, pastemxEl; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms