proposition: Lemma mantissa_digits_correct : forall x, valid_mantissa x -> EtoZ (mantissa_digits x) = Zpos (count_digits radix (MtoP x)).
proof: Proof. intros x _. rewrite <- digits_conversion. rewrite <- Digits.Zdigits2_Zdigits. unfold EtoZ, mantissa_digits, MtoP, Digits.Zdigits2. replace (Zpos (Digits.digits2_pos x)) with (Zpos (Digits.digits2_pos x) + 1 - 1)%Z by ring. generalize xH at 1 2. induction x ; intros p ; simpl digits_aux ; simpl Digits.digits2_pos. rewrite IHx, 2!Pos2Z.inj_succ. ring. rewrite IHx, 2!Pos2Z.inj_succ. ring. ring. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig