proposition: Lemma perm_free X Y : perm_eq X Y -> free X = free Y.
proof: Proof. by move=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)