proposition: Theorem generic_inclusion_le : forall e2, ( forall e, (e <= e2)%Z -> (fexp2 e <= fexp1 e)%Z ) -> forall x, (Rabs x <= bpow e2)%R -> generic_format fexp1 x -> generic_format fexp2 x.
proof: Proof. intros e2 He x [Hx|Hx]. apply generic_inclusion_mag. intros Zx. apply He. now apply mag_le_bpow. apply generic_inclusion with (e := e2). apply He. apply Z.le_refl. rewrite Hx. split. apply bpow_le. apply Zle_pred. apply Rle_refl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop