proposition: Lemma mx_col'_rcast : forall n1 n2, 'I_n2 -> (n1 + n2.-1)%N === (n1 + n2).-1.
proof: Proof. by move=> n1 n2 [j]; move/ltn_predK <-; rewrite addnS. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms