proposition: Lemma mantissa_shl_correct : forall x y z, valid_mantissa y -> EtoZ z = Zpos x -> MtoP (mantissa_shl y z) = shift radix (MtoP y) x /\ valid_mantissa (mantissa_shl y z).
proof: Proof. intros x y z (py, Vy) Hz. unfold mantissa_shl, MtoP, valid_mantissa. rewrite BigN.spec_shiftl, Vy. enough (Z.shiftl (Zpos py) (BigN.to_Z (BigZ.to_N z)) = Zpos (shift radix py x))%Z as ->. repeat split. refl_exists. unfold EtoZ in Hz. rewrite spec_to_Z, Hz. rewrite Z.shiftl_mul_pow2 by easy. rewrite shift_correct. now rewrite Z.pow_pos_fold. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig