proposition: Lemma mantissa_div_correct : forall x y, valid_mantissa x -> valid_mantissa y -> (Zpos (MtoP y) <= Zpos (MtoP x))%Z -> let (q,l) := mantissa_div x y in Zpos (MtoP q) = (Zpos (MtoP x) / Zpos (MtoP y))%Z /\ Bracket.inbetween_int (Zpos (MtoP q)) (IZR (Zpos (MtoP x)) / IZR (Zpos (MtoP y)))%R (convert_location_inv l) /\ valid_mantissa q.
proof: Proof. intros x y [x' Vx] [y' Vy]. unfold MtoP. rewrite Vx, Vy. unfold mantissa_div, mantissa_split_div. generalize (BigN.spec_div_eucl x y). generalize (Z_div_mod (Z.pos (MtoP x)) (Z.pos (MtoP y)) (eq_refl Gt)). unfold MtoP. rewrite Vx, Vy. destruct BigN.div_eucl as [q r]. destruct Z.div_eucl as [q' r']. intros [H1 H2] H. injection H. clear H. intros Hr' Vq Hxy. assert (H: (0 < q')%Z). apply Zmult_lt_reg_r with (Zpos y'). easy. rewrite Zmult_0_l, Zmult_comm. apply Zplus_lt_reg_r with r'. rewrite Zplus_0_l. rewrite <- H1. now apply Z.lt_le_trans with (2 := Hxy). destruct q' as [|q'|q'] ; try easy. rewrite Vq. clear H Hxy. assert (Hq := Zdiv_unique _ _ _ _ H2 H1). refine (conj Hq (conj _ (ex_intro _ _ Vq))). unfold Bracket.inbetween_int. rewrite BigN.spec_eqb. rewrite BigN.spec_compare. rewrite BigN.spec_shiftl_pow2. rewrite Hr', Vy. change (BigN.to_Z 0) with Z0. change (2 ^ (BigN.to_Z 1))%Z with 2%Z. destruct (Z.eqb_spec r' 0) as [Hr|Hr]. - apply Bracket.inbetween_Exact. rewrite H1, Hq, Hr, Zplus_0_r. rewrite mult_IZR. field. now apply IZR_neq. - replace (convert_location_inv _) with (Bracket.loc_Inexact (Z.compare (r' * 2) (Zpos y'))). 2: now case Z.compare. apply Bracket.inbetween_Inexact. unfold Rdiv. rewrite H1, Zmult_comm. split ; apply Rmult_lt_reg_r with (IZR (Zpos y')) ; (try now apply IZR_lt) ; rewrite Rmult_assoc, Rinv_l, Rmult_1_r, <- mult_IZR ; (try now apply IZR_neq) ; apply IZR_lt. clear -H2 Hr ; lia. rewrite Zmult_plus_distr_l. clear -H2 ; lia. rewrite H1, 2!plus_IZR, mult_IZR. destruct (Z.compare_spec (r' * 2) (Zpos y')) as [H|H|H]. + apply Rcompare_Eq. rewrite <- H. rewrite mult_IZR. field. now apply IZR_neq. + apply Rcompare_Lt. apply Rminus_gt. match goal with |- (?a > 0)%R => replace a with ((IZR (Zpos y') - IZR r' * 2) / (2 * IZR (Zpos y')))%R end. apply Fourier_util.Rlt_mult_inv_pos. apply Rgt_minus. rewrite <- mult_IZR. now apply IZR_lt. apply Rmult_lt_0_compat. apply Rlt_0_2. now apply IZR_lt. field. now apply IZR_neq. + apply Rcompare_Gt. apply Rminus_lt. match goal with |- (?a < 0)%R => replace a with (- ((IZR r' * 2 - IZR (Zpos y')) / (2 * IZR (Zpos y'))))%R end. apply Ropp_lt_gt_0_contravar. apply Fourier_util.Rlt_mult_inv_pos. apply Rgt_minus. rewrite <- mult_IZR. now apply IZR_lt. apply Rmult_lt_0_compat. apply Rlt_0_2. now apply IZR_lt. field. now apply IZR_neq. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig