proposition: Lemma mantissa_shrp_aux_correct m d : mantissa_shrp_aux m (Pos.succ d) = match (m ?= shift radix 1 d)%positive with | Eq => pos_Mi | _ => pos_Up end.
proof: Proof. apply eq_trans with (if (m =? shift radix 1 d)%positive then pos_Mi else pos_Up); last first. now rewrite Pos.eqb_compare; destruct Pos.compare. rewrite Pos2Z.inj_eqb, shift_correct, Z.pow_pos_fold, Zmult_1_l. rewrite <- radix_to_pos, <- Pos2Z.inj_pow. revert d; induction m as [m|m|]; intros d. - case (Pos.succ_pred_or d); intro Hd. now rewrite Hd; simpl; destruct m. rewrite <- Hd, Pos.pow_succ_r. now unfold mantissa_shrp_aux; case Pos.eqb. - case (Pos.succ_pred_or d); intro Hd. now rewrite Hd; destruct m. rewrite <- Hd at 2. rewrite Pos.pow_succ_r. rewrite <- Pos2Z.inj_eqb, Pos.eqb_compare, Pos.compare_xO_xO. rewrite <- Pos.eqb_compare, Pos2Z.inj_eqb, <- IHm; simpl. now rewrite Hd, Pos.pred_succ; destruct d. case (Pos.succ_pred_or d); intro Hd. now rewrite Hd. rewrite <- Hd at 2. rewrite Pos.pow_succ_r. now destruct d. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig