proposition: Lemma similar_cast n m p (eq1 : m = p) (eq2 : m = p) (A : 'M[R]_n) (B : 'M[R]_m) : similar A (castmx (eq1,eq2) B) <-> similar A B.
proof: Proof. by case: _ /eq1 eq2=> eq2; rewrite castmx_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring