proposition: Theorem generic_inclusion_mag : forall x, ( x <> 0%R -> (fexp2 (mag beta x) <= fexp1 (mag beta x))%Z ) -> generic_format fexp1 x -> generic_format fexp2 x.
proof: Proof. intros x He Fx. rewrite Fx. apply generic_format_F2R. intros Zx. rewrite <- Fx. apply He. contradict Zx. rewrite Zx, scaled_mantissa_0. apply Ztrunc_IZR. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop