proposition: Theorem div_aa : forall x y : R, forall xi yi zi : FF, ABS x xi -> ABS y yi -> div_aa_helper xi yi zi = true -> ABS (x / y) zi.
proof: Proof. intros x y xi yi zi Hx Hy 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 (Hb,H2). generalize (Fpos_correct _ Hb). intro H1. generalize (Fpos0_correct _ H2). clear H2. intro H2. generalize (Fle2_correct _ _ H3). rewrite Fmult2_correct. clear H3. intro H3. generalize (Fle2_correct _ _ H4). rewrite Fmult2_correct. clear H4. intro H4. split. exact H2. replace (Rabs (x / y)) with (Rabs x / Rabs y)%R. unfold ABS in *. apply IRdiv_pp with (lower xi) (upper xi) (lower yi) (upper yi) ; intuition. unfold Rdiv. rewrite Rabs_mult. rewrite Rabs_Rinv. apply refl_equal. apply nzr_of_abs with (1 := Hy) (2 := Hb). Qed.
imports: Gappa_common Gappa_pred_nzr