proposition: Lemma linear_closedB : linear_closed -> subr_2closed S.
proof: Proof. by move=> Slin u v Su Sv; rewrite addrC -scaleN1r Slin. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)