proposition: Theorem bnd_div_of_rel_bnd_div : forall x1 x2 y : R, forall xi yi zi : FF, REL x1 x2 xi -> BND (x2 / y) yi -> NZR y -> mul_helper xi yi zi = true -> BND ((x1 - x2) / y) zi.
proof: Proof. intros x1 x2 y xi yi zi (ex,(Hx1,Hx2)) Hxy Zy Hb. rewrite Hx2. replace ((x2 * (1 + ex) - x2) / y)%R with (ex * (x2 / y))%R by now field. 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). apply Fle2_correct in H1. apply Fle2_correct in H2. apply Fle2_correct in H3. apply Fle2_correct in H4. assert (H5 := FImult2_correct (lower xi) yi _ Hxy). assert (H6 := FImult2_correct (upper xi) yi _ Hxy). destruct (Rle_or_lt 0 (x2 / y)) as [Hy|Hy]. split. apply Rle_trans with (1 := H1). apply Rle_trans with (1 := proj1 H5). now apply monotony_2p. apply Rle_trans with (2 := H4). apply Rle_trans with (2 := proj2 H6). now apply monotony_2p. apply Rlt_le in Hy. split. apply Rle_trans with (1 := H2). apply Rle_trans with (1 := proj1 H6). now apply monotony_2n. apply Rle_trans with (2 := H3). apply Rle_trans with (2 := proj2 H5). now apply monotony_2n. Qed.
imports: Gappa_common Gappa_pred_bnd