proposition: Theorem generic_inclusion_le_ge : forall e1 e2, (e1 < e2)%Z -> ( 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' He x (Hx1,[Hx2|Hx2]). apply generic_inclusion_mag. intros Zx. apply He. split. now apply mag_gt_bpow. now apply mag_le_bpow. apply generic_inclusion with (e := e2). apply He. split. apply He'. apply Z.le_refl. rewrite Hx2. split. apply bpow_le. apply Zle_pred. apply Rle_refl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop