proposition: Lemma div2_correct : forall x, sensible_format = true -> (1 / 256 <= Rabs (toR x))%R -> toX (div2 x) = Xdiv (toX x) (Xreal 2).
proof: Proof. intros x Hf _. unfold div2, Fdiv2, toX. rewrite Fscale2_correct; [|easy]. simpl; unfold Z.pow_pos; simpl. rewrite Xdiv_split. unfold Xinv, Xinv'. now rewrite is_zero_false. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig