proposition: Lemma span_cat X Y : (<<X ++ Y>> = <<X>> + <<Y>>)%VS.
proof: Proof. by rewrite !span_def big_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)