proposition: Lemma scaler_injl : {in unit, @right_injective R A A *:%R}.
proof: Proof. move=> k Uk x1 x2 Hx1x2. by rewrite -[x1]scale1r -(mulVr Uk) -scalerA Hx1x2 scalerA mulVr // scale1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)