proposition: Lemma double_monotone a b: natp a -> natp b -> (cdouble a <=c cdouble b <-> a <=c b).
proof: Proof. move => pa pb; rewrite /cdouble. split; [apply:(cprod_le2l NS2 pa pb card2_nz) | apply: cprod_Meqle]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)