proposition: Lemma rpredBC u v : u - v \in S = (v - u \in S).
proof: Proof. by rewrite -rpredN opprB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)