proposition: Lemma rpredN : {mono -%R: u / u \in S}.
proof: Proof. by move=> u; apply/idP/idP=> /rpredNr; rewrite ?opprK; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)