proposition: Theorem sub_flt : forall x y xn yn xyi zn, FLT x xn -> FLT y yn -> REL x y xyi -> sub_flt_helper xn yn zn xyi = true -> FLT (x - y) zn.
proof: Proof. intros x y xn yn xyi zn Hx Hy (eps,((Hxy1,Hxy2),Hxy3)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H4). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H3). clear H3. intro H3. generalize (Fle2_correct _ _ H4). clear H4. intro H4. destruct (total_order_T y 0) as [[Zy|Zy]|Zy]. apply <- FLT_iff_generic. unfold Rminus. rewrite <- (Ropp_involutive x), Rplus_comm. apply sterbenz. now apply FLX_exp_valid. apply FLX_exp_monotone. apply generic_format_opp. apply -> FLT_iff_generic. now apply flt_subset with yn. apply generic_format_opp. apply -> FLT_iff_generic. now apply flt_subset with xn. rewrite Hxy3, <- Ropp_mult_distr_l_reverse. unfold Rdiv. rewrite (Rmult_comm 2), 2!Rmult_assoc. pattern (-y)%R at 2 3 ; rewrite <- Rmult_1_r. assert (Zy': (0 <= -y)%R). apply Rlt_le. now apply Ropp_0_gt_lt_contravar. split ; apply Rmult_le_compat_l ; try easy. apply Rmult_le_reg_r with 2%R. now apply IZR_lt. rewrite Rmult_assoc, Rinv_l, Rmult_1_l, Rmult_1_r. apply (Rplus_le_compat_l _ _ 1%R). apply Rle_trans with (1 := Hxy2). now rewrite <- (Rmult_1_r 1). apply Rgt_not_eq. now apply IZR_lt. replace 1%R with ((1 + -1 / 2)*2)%R at 1 by field. apply Rmult_le_compat_r. now apply IZR_le. apply Rplus_le_compat_l. now apply Rle_trans with (2 := Hxy1). rewrite Zy, Rminus_0_r. now apply flt_subset with xn. apply <- FLT_iff_generic. apply sterbenz. now apply FLX_exp_valid. apply FLX_exp_monotone. apply -> FLT_iff_generic. now apply flt_subset with xn. apply -> FLT_iff_generic. now apply flt_subset with yn. rewrite Hxy3. unfold Rdiv. rewrite (Rmult_comm 2). assert (Zy': (0 <= y)%R). now apply Rlt_le. split ; apply Rmult_le_compat_l ; try easy. replace (/2)%R with (1 + -1/2)%R by field. apply Rplus_le_compat_l. now apply Rle_trans with (2 := Hxy1). apply (Rplus_le_compat_l _ _ 1%R). apply Rle_trans with (1 := Hxy2). now rewrite <- (Rmult_1_r 1). Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux