proposition: Lemma FalgType_proper : dim aT > 0.
proof: Proof. rewrite lt0n; apply: contraNneq (oner_neq0 aT) => aT0. by apply/eqP/v2r_inj; do 2!move: (v2r _); rewrite aT0 => u v; rewrite !thinmx0. 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)