proposition: Lemma sub_scale_ball A k l : k <= l -> k *` A `<=` l *` A.
proof: Proof. move=> kl; rewrite /scale_ball; case: ifPn=> [Aball|_]; last exact: subset_refl. by apply: le_ball; rewrite ler_wpM2r. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule