proposition: Lemma scaler_eq0 a v : (a *: v == 0) = (a == 0) || (v == 0).
proof: Proof. have [-> | nz_a] := eqVneq a; first by rewrite scale0r eqxx. by rewrite (can2_eq (scalerK nz_a) (scalerKV nz_a)) scaler0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)