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