proposition: Lemma mantissa_sqrt_correct : forall x, valid_mantissa x -> let (q,l) := mantissa_sqrt x in let (s,r) := Z.sqrtrem (Zpos (MtoP x)) in Zpos (MtoP q) = s /\ match l with pos_Eq => r = Z0 | pos_Lo => (0 < r <= s)%Z | pos_Mi => False | pos_Up => (s < r)%Z end /\ valid_mantissa q.
proof: Proof. intros x _. unfold mantissa_sqrt, MtoP. refine (_ (Z.sqrtrem_spec (Zpos x) _)). 2: easy. case Z.sqrtrem. intros s r [H1 H2]. destruct s as [|s|s]. simpl in H1. rewrite <- H1 in H2. now elim (proj2 H2). repeat split. destruct r as [|r|r]. apply eq_refl. case Pos.compare_spec. intros ->. split. easy. apply Z.le_refl. intros H. split. easy. now apply Zlt_le_weak. easy. now elim (proj1 H2). now elim (Z.le_trans _ _ _ (proj1 H2) (proj2 H2)). Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig