proposition: Lemma FLT_format_double: forall u, format u -> format (2*u).
proof: Proof. Proof with auto with typeclass_instances. intros u Fu. apply generic_format_FLT. apply FLT_format_generic in Fu... destruct Fu as [uf H1 H2 H3]. exists (Float radix2 (Fnum uf) (Fexp uf+1)). rewrite H1; unfold F2R; simpl. rewrite bpow_plus, bpow_1. simpl;ring. easy. apply Z.le_trans with (1:=H3). apply Zle_succ. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)