proposition: Lemma add_slow_aux2_correct : forall mode p sx sy mx my ex ey, valid_mantissa mx -> valid_mantissa my -> FtoX (toF (add_slow_aux2 mode p sx sy mx my ex ey)) = FtoX (Fround_at_prec mode (prec p) (Fadd_slow_aux2 radix sx sy (MtoP mx) (MtoP my) (EtoZ ex) (EtoZ ey) pos_Eq)).
proof: Proof. intros mode p sx sy mx my ex ey Vx Vy. unfold add_slow_aux2, Fadd_slow_aux2. rewrite exponent_cmp_correct, exponent_sub_correct, exponent_zero_correct. case_eq (EtoZ ex - EtoZ ey)%Z ; unfold Z.compare. - intros _. now apply add_slow_aux1_correct. - intros d Hd. generalize (mantissa_shl_correct d mx (exponent_sub ex ey) Vx). intros H'. destruct H' as [H1 H2]. rewrite <- Hd. apply exponent_sub_correct. rewrite add_slow_aux1_correct by assumption. now rewrite H1. - intros d Hd. generalize (mantissa_shl_correct d my (exponent_neg (exponent_sub ex ey)) Vy). intros H'. destruct H' as [H1 H2]. change (Zpos d) with (Z.opp (Zneg d)). rewrite <- Hd. rewrite exponent_neg_correct. apply f_equal, exponent_sub_correct. rewrite add_slow_aux1_correct by assumption. now rewrite H1. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig