proposition: Theorem mul_oo : forall x y : R, forall xi yi zi : FF, BND x xi -> BND y yi -> mul_oo_helper xi yi zi = true -> BND (x * y) zi.
proof: Proof. intros x y xi yi zi Hx Hy Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H8). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H7). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H6). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H5). 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 (Fneg0_correct _ H1). clear H1. intro H1. generalize (Fpos0_correct _ H2). clear H2. intro H2. generalize (Fneg0_correct _ H3). clear H3. intro H3. generalize (Fpos0_correct _ H4). clear H4. intro H4. generalize (Fle2_correct _ _ H5). rewrite Fmult2_correct. clear H5. intro H5. generalize (Fle2_correct _ _ H6). rewrite Fmult2_correct. clear H6. intro H6. generalize (Fle2_correct _ _ H7). rewrite Fmult2_correct. clear H7. intro H7. generalize (Fle2_correct _ _ H8). rewrite Fmult2_correct. clear H8. intro H8. exact (IRmult_oo _ _ _ _ _ _ H1 H2 H3 H4 H6 H5 H7 H8 _ _ Hx Hy). Qed.
imports: Gappa_common Gappa_decimal