proposition: Theorem generic_inclusion_ge : forall e1, ( forall e, (e1 < e)%Z -> (fexp2 e <= fexp1 e)%Z ) -> forall x, (bpow e1 <= Rabs x)%R -> generic_format fexp1 x -> generic_format fexp2 x.
proof: Proof. intros e1 He x Hx. apply generic_inclusion_mag. intros Zx. apply He. now apply mag_gt_bpow. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop