proposition: Lemma double_le_odd1 p k: natp k -> natp p -> cdouble p <=c csucc (cdouble k) -> p <=c k.
proof: Proof. move => kN pN le1; case:(NleT_el pN kN) => // /(cleSltP kN). move/(double_monotone (NS_succ kN) pN);rewrite (double_succ kN) => le2. case: (cleNgt le2 (cle_ltT le1 (cltS (NS_succ (NS_double kN))))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)