proposition: Lemma add_slow_aux1_correct : forall mode p sx sy mx my e, valid_mantissa mx -> valid_mantissa my -> FtoX (toF (add_slow_aux1 mode p sx sy mx my e)) = FtoX (Fround_at_prec mode (prec p) (Fadd_slow_aux1 radix sx sy (MtoP mx) (MtoP my) (EtoZ e) pos_Eq)).
proof: Proof. intros mode p sx sy mx my e Vx Vy. unfold add_slow_aux1, Fadd_slow_aux1. case eqb. - destruct (mantissa_add_correct mx my Vx Vy) as [H1 H2]. rewrite <- H1. now apply round_aux_correct. - change (Zpos (MtoP mx) + Zneg (MtoP my))%Z with (Zpos (MtoP mx) - Zpos (MtoP my))%Z. rewrite (mantissa_cmp_correct mx my Vx Vy). rewrite Z.compare_sub. case_eq (Zpos (MtoP mx) - Zpos (MtoP my))%Z ; unfold Z.compare. + intros H. simpl. generalize (mantissa_sign_correct mantissa_zero). case mantissa_sign. easy. rewrite mantissa_zero_correct. now intros [|]. + intros m H. assert (H': (Zpos (MtoP my) < Zpos (MtoP mx))%Z). clear -H ; lia. destruct (mantissa_sub_correct mx my Vx Vy H') as [H1 H2]. rewrite round_aux_correct by exact H2. rewrite H1. simpl in H. rewrite Z.pos_sub_gt in H by exact H'. injection H. now intros ->. + intros m H. assert (H': (Zpos (MtoP mx) < Zpos (MtoP my))%Z). clear -H ; lia. destruct (mantissa_sub_correct my mx Vy Vx H') as [H1 H2]. rewrite round_aux_correct by exact H2. rewrite H1. simpl in H. rewrite Z.pos_sub_lt in H by exact H'. injection H. now intros ->. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig