proposition: Lemma double_monotone3 a b: natp a -> natp b -> (csucc (cdouble a) <c cdouble b <-> a <c b).
proof: Proof. move => aN bN. move:(cleSltP (NS_succ (NS_double aN)) (cdouble b)); rewrite -(double_succ aN). move:(iff_trans (double_monotone (NS_succ aN) bN) (cleSltP aN b)). move => ha hb; exact (iff_trans (iff_sym hb) ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)