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, sm1. rewrite scale2_correct; [|easy]. simpl; unfold Z.pow_pos; simpl. rewrite Xdiv_split. unfold Xinv, Xinv'. unfold StoZ. rewrite ZtoE_correct. now rewrite is_zero_false. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig