proposition: Lemma cat_free X Y : free (X ++ Y) = [&& free X, free Y & directv (<<X>> + <<Y>>)].
proof: Proof. rewrite !free_directv mem_cat directvE /= !big_cat -directvE directv_addE /=. rewrite negb_or -!andbA; do !bool_congr; rewrite -!span_def. by rewrite (sameP eqP directv_addP). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)