proposition: Lemma add_slow_correct : forall mode p x y, toX (add_slow mode p x y) = Xround radix mode (prec p) (Xadd (toX x) (toX y)).
proof: Proof. intros mode p x y. unfold toX. rewrite <- Fadd_correct. unfold add_slow, Fadd_slow, Fadd_slow_aux. destruct x as [|mx ex] ; try easy. destruct y as [|my ey]. simpl. now destruct (mantissa_sign mx). unfold toF. generalize (mantissa_sign_correct mx). case_eq (mantissa_sign mx). - intros Hx _. generalize (mantissa_sign_correct my). destruct (mantissa_sign my) as [|sy ny]. now rewrite Hx. intros [My Vy]. rewrite <- round_aux_correct by exact Vy. case round_aux. reflexivity. intros m e. generalize (mantissa_sign_correct m). case_eq (mantissa_sign m). simpl. now intros ->. intros s n. simpl. now intros ->. - intros sx nx Hx [Hmx Vx]. generalize (mantissa_sign_correct my). destruct (mantissa_sign my) as [|sy ny]. + intros Hy. rewrite <- round_aux_correct by exact Vx. case round_aux. reflexivity. intros m e. generalize (mantissa_sign_correct m). case_eq (mantissa_sign m). simpl. now intros ->. intros s n. simpl. now intros ->. + intros [Hmy Vy]. rewrite <- (add_slow_aux2_correct mode p sx sy nx ny ex ey Vx Vy). case add_slow_aux2. reflexivity. intros m e. generalize (mantissa_sign_correct m). case_eq (mantissa_sign m). simpl. now intros ->. simpl. now intros s n ->. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig