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