proposition: Lemma mantissa_shl_correct : forall x y z, valid_mantissa y -> z = Zpos x -> MtoP (mantissa_shl y z) = shift radix (MtoP y) x /\ valid_mantissa (mantissa_shl y z).
proof: Proof. repeat split. unfold EtoZ in H0. rewrite H0. apply refl_equal. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig