proposition: Lemma b_power_k_large a b: natp a -> natp b -> \1c <c b -> a <> \0c -> exists k, [/\ natp k, (b ^c k) <=c a & a <c (b ^c (csucc k))].
proof: Proof. move=> aN bN l1b naz. pose prop x := a <c (b ^c x). have exp: prop a by apply: cpow_M1lt;fprops. case: (least_int_prop2 aN exp). rewrite /prop cpowx0 => a1; case(cltNge a1 (cge1 (CS_nat aN) naz)). set k := cpred _; move => [kN pks npk]. exists k; split => //. by case: (NleT_el (NS_pow bN kN) aN) => // h; case: npk. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)