proposition: Lemma raddfN : {morph f : x / - x}.
proof: Proof. move=> x. by rewrite -[LHS]addr0 -(subrr (f x)) addrA -raddfD addNr raddf0 sub0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)