proposition: Theorem generic_inclusion : forall e, (fexp2 e <= fexp1 e)%Z -> forall x, (bpow (e - 1) <= Rabs x <= bpow e)%R -> generic_format fexp1 x -> generic_format fexp2 x.
proof: Proof. Proof with auto with typeclass_instances. intros e He x (Hx1,[Hx2|Hx2]). apply generic_inclusion_mag. now rewrite mag_unique with (1 := conj Hx1 Hx2). intros Fx. apply generic_format_abs_inv. rewrite Hx2. apply generic_format_bpow'... apply Z.le_trans with (1 := He). apply generic_format_bpow_inv... rewrite <- Hx2. now apply generic_format_abs. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop