proposition: Lemma scaler_unit k x : k \in unit -> (k *: x \in unit) = (x \in unit).
proof: Proof. move=> Uk; apply/idP/idP=> [Ukx | Ux]; apply/unitrP; last first. exists (k^-1 *: x^-1). by rewrite -!scalerAl -!scalerAr !scalerA !mulVr // !mulrV // scale1r. exists (k *: (k *: x)^-1); split. apply: (mulrI Ukx). by rewrite mulr1 mulrA -scalerAr mulrV // -scalerAl mul1r. apply: (mulIr Ukx). by rewrite mul1r -mulrA -scalerAl mulVr // -scalerAr mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)