proposition: Lemma raddfZnat n u : h (n%:R *: u) = n%:R *: h u.
proof: Proof. by rewrite !scaler_nat raddfMn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)