proposition: Lemma adim_gt0 A : (0 < \dim A)%N.
proof: Proof. by rewrite -(dim_algid A) dimvS // -memvE ?memv_algid. 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)