proposition: Lemma cexp_ge_bpow : forall (x : R) (e : Z), (bpow (e - 1) <= Rabs x)%R -> (fexp e <= cexp x)%Z.
proof: Proof. intros x e Hx. apply monotone_exp. rewrite (Zsucc_pred e). apply Zlt_le_succ. now apply mag_gt_bpow. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop