proposition: Lemma half_monotone2 n m: natp n -> natp m -> n <=c (chalf m) -> cdouble n <=c m.
proof: Proof. move => nN mN; move /(double_monotone nN (NS_half mN)) => sa. case: (cdouble_halfV mN) => -> //. exact:(cleT sa (cleS (NS_double (NS_half mN)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)