proposition: Lemma raddfZsign n u : h ((-1) ^+ n *: u) = (-1) ^+ n *: h u.
proof: Proof. by rewrite !(scaler_sign, =^~ signr_odd) (fun_if h) raddfN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)