proposition: Lemma dim_prodv U V : \dim (U * V) <= \dim U * \dim V.
proof: Proof. by rewrite unlock (leq_trans (dim_span _)) ?size_tuple. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)