proposition: Lemma adim1P {A} : reflect (A = <[algid A]>%VS :> {vspace aT}) (\dim A == 1%N).
proof: Proof. rewrite eqn_leq adim_gt0 -(memv_algid A) andbC -(dim_algid A) -eqEdim eq_sym. exact: eqP. 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)