proposition: Lemma half_monotone n m: natp n -> natp m -> n <=c m -> chalf n <=c chalf m.
proof: Proof. move => nN mN. move:(NS_half nN) (NS_half mN) => hnN hmN. case: (cdouble_halfV nN) => {1} ->;case: (cdouble_halfV mN) => {1} ->. + by move/(double_monotone hnN hmN). + move/(cltSleP (NS_succ (NS_double hmN))); rewrite - (double_succ hmN). by move/(double_monotone2 hnN (NS_succ hmN)); move/(cltSleP hmN). + by move/(cleT (cleS (NS_double hnN))) /(double_monotone hnN hmN). + move/(cleSSP (CS_nat(NS_double hnN)) (CS_nat (NS_double hmN))). by move/(double_monotone hnN hmN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)