proposition: Lemma exists_frac_part (P : nat -> Prop) : (exists n, P n) -> forall num den, (0 < num)%nat -> (0 < den)%nat -> (forall n m, (n <= m)%nat -> P n -> P m) -> exists n, P n /\ frac_part (exp2 (n%:R * (log num%:R / den%:R))) = 0.
proof: Proof. case=> n Pn num den Hden HP. exists (n * den)%nat. split. apply H with n => //. by rewrite -{1}(muln1 n) leq_mul2l HP orbC. rewrite natRM -mulRA (mulRCA den%:R) mulRV // ?mulR1; last first. by rewrite INR_eq0' -lt0n. by rewrite exp2_pow logK; [exact/frac_part_pow/frac_part_INR | exact/ltR0n]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext