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 _ _. unfold MtoP. intros Hxy. unfold mantissa_div, mantissa_split_div. generalize (Z_div_mod (Z.pos x) (Z.pos y) (eq_refl Gt)). rewrite Zfast_div_eucl_correct. destruct Z.div_eucl as [q r]. intros [H1 H2]. 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. clear H Hxy. assert (Hq := Zdiv_unique _ _ _ _ H2 H1). refine (conj Hq (conj _ I)). unfold Bracket.inbetween_int. destruct (Zle_or_lt 2 (Zpos y)) as [Hy|Hy]. - assert (H: (1 < Zpos y)%Z) by now apply Z.gt_lt, Zle_succ_gt. rewrite adjust_pos_correct by assumption. rewrite plus_IZR. rewrite <- (Rinv_r (IZR (Zpos y))) by now apply IZR_neq. apply Bracket.new_location_correct ; try assumption. now apply Rinv_0_lt_compat, IZR_lt. apply Bracket.inbetween_Exact. rewrite H1, plus_IZR, mult_IZR. field. now apply IZR_neq. - rewrite Hq, H1. clear H1 Hq. cut (Zpos y = 1 /\ r = 0)%Z. 2: lia. clear. intros [-> ->]. simpl. apply Bracket.inbetween_Exact. unfold Rdiv. now rewrite Zdiv_1_r, Rinv_1, Rmult_1_r. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig