proposition: Lemma Fadd_slow_aux1_correct : forall beta sx sy mx my e, UtoX (Fadd_slow_aux1 beta sx sy mx my e pos_Eq) = Xadd (FtoX (@Float beta sx mx e)) (FtoX (@Float beta sy my e)).
proof: Proof. intros. simpl Xbind2. unfold Fadd_slow_aux1. change (Zpos mx + Zneg my)%Z with (Zpos mx - Zpos my)%Z. case_eq (eqb sx sy) ; intro H. rewrite (eqb_prop _ _ H). rewrite FtoR_add. apply refl_equal. replace sy with (negb sx). clear H. case_eq (Zpos mx - Zpos my)%Z. intro H. rewrite <- (FtoR_neg beta sx). unfold FtoR. change (Zneg mx) with (- Zpos mx)%Z. rewrite (Zminus_eq _ _ H). rewrite Rplus_opp_r. apply refl_equal. intro p. unfold Zminus, Zplus. simpl. rewrite Z.pos_sub_spec. case_eq (mx ?= my)%positive ; intros ; try discriminate H0. rewrite (FtoR_sub beta sx). now inversion H0. apply Z.gt_lt. exact H. intro p. unfold Zminus, Zplus. simpl. rewrite Z.pos_sub_spec. case_eq (mx ?= my)%positive ; intros ; try discriminate H0. pattern sx at 2 ; rewrite <- (negb_involutive sx). rewrite Rplus_comm. rewrite (FtoR_sub beta (negb sx)). now inversion H0. exact H. generalize H. clear. now case sx ; case sy. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic