proposition: Lemma invrZ k x : k \in unit -> x \in unit -> (k *: x)^-1 = k^-1 *: x^-1.
proof: Proof. move=> Uk Ux; have Ukx: (k *: x \in unit) by rewrite scaler_unit. apply: (mulIr Ukx). by rewrite mulVr // -scalerAl -scalerAr scalerA !mulVr // scale1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)