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. intros x d Vx. repeat split. exact Vx. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig