proposition: Lemma t4_exact_: t4=c-(a-b).
proof: Proof. Proof with auto with typeclass_instances. unfold t4; rewrite ab_exact_. case cPos; intros K. apply round_generic... assert (H:(generic_format beta (FLX_exp prec) c)). now apply generic_format_FLX_FLT with emin. apply FLXN_format_generic in H... destruct H as [fc Hfc1 Hfc2]. case (Zle_or_lt emin (Fexp fc)); intros Y. apply t4_exact_aux_ with fc. apply Hfc2. now apply Rgt_not_eq. split. apply Rle_0_minus. apply Rplus_le_reg_l with b; ring_simplify. exact isaTriangle1. rewrite <-Hfc1. apply Rplus_le_reg_l with (-c+a); ring_simplify. exact bLea. apply generic_format_FLX_FLT in Fa. apply FLXN_format_generic in Fa... destruct Fa as [fa Hfa1 Hfa2]. apply generic_format_FLX_FLT in Fb. apply FLXN_format_generic in Fb... destruct Fb as [fb Hfb1 Hfb2]. exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc) -Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z. rewrite Hfa1, Hfb1, Hfc1; unfold F2R; simpl. rewrite 2!minus_IZR. rewrite 2!mult_IZR. rewrite 2!IZR_Zpower. unfold Zminus; rewrite 2!bpow_plus. rewrite bpow_opp. field. apply Rgt_not_eq. apply bpow_gt_0. assert (Fexp fc <= Fexp fb)%Z. 2: lia. apply FLXN_le_exp with prec... apply Hfc2. now apply Rgt_not_eq. apply Hfb2. apply Rgt_not_eq. apply Rlt_le_trans with c; assumption. rewrite <- Hfc1; assumption. rewrite <- Hfc1, <-Hfb1; assumption. assert (Fexp fc <= Fexp fa)%Z. apply FLXN_le_exp with prec... apply Hfc2. now apply Rgt_not_eq. apply Hfa2. apply Rgt_not_eq. apply Rlt_le_trans with c; try assumption. apply Rle_trans with b; assumption. rewrite <- Hfc1; assumption. rewrite <- Hfc1, <-Hfa1. apply Rle_trans with b; assumption. lia. assumption. assert (exists f:float beta, c = F2R f /\ Fexp f = emin /\ (Z.abs (Fnum f) < beta ^ prec)%Z). apply FLT_format_generic in Fc... destruct Fc as [ffc Hffc1 Hffc2 Hffc3]. exists (Float beta (Fnum ffc*Zpower beta (Fexp ffc-emin)) emin). split. rewrite Hffc1; unfold F2R; simpl. rewrite mult_IZR, IZR_Zpower. unfold Zminus; rewrite bpow_plus, bpow_opp. field. apply Rgt_not_eq. apply bpow_gt_0. lia. split. reflexivity. simpl. apply lt_IZR. rewrite abs_IZR, mult_IZR, IZR_Zpower. 2: lia. unfold Zminus; rewrite bpow_plus, <- Rmult_assoc. replace (IZR (Fnum ffc) * bpow (Fexp ffc)) with (F2R ffc) by reflexivity. rewrite <- Hffc1. rewrite Hfc1; unfold F2R; rewrite Rmult_assoc, <- bpow_plus. rewrite Rabs_mult. apply Rle_lt_trans with (Rabs (IZR (Fnum fc)) *1). apply Rmult_le_compat_l. apply Rabs_pos. rewrite Rabs_right. 2: apply Rle_ge, bpow_ge_0. replace 1 with (bpow 0) by reflexivity. apply bpow_le. lia. rewrite Rmult_1_r. rewrite <- abs_IZR. apply IZR_lt. apply Hfc2. now apply Rgt_not_eq. destruct H as (gc,(Hgc1,(Hgc2,Hgc3))). apply t4_exact_aux_ with gc. assumption. split. apply Rle_0_minus. apply Rplus_le_reg_l with b; ring_simplify. exact isaTriangle1. rewrite <-Hgc1. apply Rplus_le_reg_l with (-c+a); ring_simplify. exact bLea. apply FLT_format_generic in Fa... destruct Fa as [fa Hfa1 Hfa2 Hfa3]. apply FLT_format_generic in Fb... destruct Fb as [fb Hfb1 Hfb2 Hfb3]. rewrite Hgc2. exists (Fnum gc -(Fnum fa*Zpower beta (Fexp fa-emin) -Fnum fb*Zpower beta (Fexp fb -emin)))%Z. rewrite Hfa1, Hfb1, Hgc1; unfold F2R; simpl. rewrite Hgc2, 2!minus_IZR. rewrite 2!mult_IZR. rewrite 2!IZR_Zpower. unfold Zminus; rewrite 2!bpow_plus. rewrite bpow_opp. field. apply Rgt_not_eq. apply bpow_gt_0. lia. lia. lia. unfold Rminus; rewrite <-K, Rplus_0_l. rewrite round_NE_opp. apply f_equal. apply ab_exact_. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)