proposition: Theorem valid_exp_large : forall k l, (fexp k < k)%Z -> (k <= l)%Z -> (fexp l < l)%Z.
proof: Proof. intros k l Hk H. apply Znot_ge_lt. intros Hl. apply Z.ge_le in Hl. assert (H' := proj2 (proj2 (valid_exp l) Hl) k). lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop