proposition: Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y.
proof: Proof. move=> eqXY; congr ((_ == _) && _); last exact: perm_free. exact/eq_span/perm_mem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)