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... apply FLXN_format_generic in Fc... destruct Fc as [fc Hfc1 Hfc2]. 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 FLXN_format_generic in Fa... destruct Fa as [fa Hfa1 Hfa2]. 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. 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. 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. 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)