proposition: Lemma Fadd_slow_aux2_correct : forall beta sx sy mx my ex ey, UtoX (Fadd_slow_aux2 beta sx sy mx my ex ey pos_Eq) = Xadd (FtoX (@Float beta sx mx ex)) (FtoX (@Float beta sy my ey)).
proof: Proof. intros. unfold Xbind2, FtoX. unfold Fadd_slow_aux2. case_eq (ex - ey)%Z ; intros ; rewrite Fadd_slow_aux1_correct ; unfold FtoX, Xbind2. replace ey with ex. apply refl_equal. rewrite <- (Zplus_0_l ey). rewrite <- H. ring. rewrite <- FtoR_shift. rewrite <- H. replace (ey + (ex - ey))%Z with ex. 2: ring. apply refl_equal. rewrite <- FtoR_shift. replace (ex + Zpos p)%Z with ey. apply refl_equal. change (Zpos p) with (- Zneg p)%Z. rewrite <- H. ring. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic