proposition: Lemma double_le_odd2 p k: natp k -> natp p -> csucc (cdouble k) <=c cdouble p -> csucc k <=c p.
proof: Proof. move => kN pN; move/cleSS. rewrite - (double_succ kN); apply:(double_le_odd1 pN (NS_succ kN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)