proposition: Lemma cexp_le_bpow : forall (x : R) (e : Z), x <> 0%R -> (Rabs x < bpow e)%R -> (cexp x <= fexp e)%Z.
proof: Proof. intros x e Zx Hx. apply monotone_exp. now apply mag_le_bpow. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop