proposition: Lemma mantissa_scale2_correct : forall x d, valid_mantissa x -> let (x',d') := mantissa_scale2 x d in (IZR (Zpos (MtoP x')) * bpow radix (EtoZ d') = IZR (Zpos (MtoP x)) * bpow radix2 (EtoZ d))%R /\ valid_mantissa x'.
proof: Proof. now intros x d Vx. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig