proposition: Lemma format_bpow_d: (0 < F2R d)%R -> generic_format beta fexp (bpow (mag beta (F2R d))).
proof: Proof. Proof with auto with typeclass_instances. intros Y; apply generic_format_bpow. apply valid_exp. apply mag_generic_gt... now apply Rgt_not_eq. now apply generic_format_canonical. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations