proposition: Lemma cpred_monotone a b: a <=c b -> cpred a <=c cpred b.
proof: Proof. move => [ca cb sab]; split; [exact (CS_pred ca) | exact (CS_pred cb) | ]. rewrite /cpred/opred => t /setU_P [y ya /sab yb]; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)