proposition: Theorem cexp_round_ge : forall x, round rnd x <> 0%R -> (cexp x <= cexp (round rnd x))%Z.
proof: Proof. Proof with auto with typeclass_instances. intros x Zr. unfold cexp. apply monotone_exp. now apply mag_round_ge. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop