proposition: Lemma eqid_scaleid (x: R) m n (I: 'cV[R]_m) (J: 'cV[R]_n): x != 0 -> (I == J)%IS = (x *: I == x *: J)%IS.
proof: Proof. move=> x0; apply/idP/andP=> [|[]]. by rewrite (@subid_scaleid x) //; case/andP=> ->; rewrite (@subid_scaleid x). by rewrite -(@subid_scaleid x) // => ->; rewrite -(@subid_scaleid x) // => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice fingroup) mathcomp(matrix bigop zmodp mxalgebra poly) ssrcomplements