proposition: Theorem mul_aa : forall x y : R, forall xi yi zi : FF, ABS x xi -> ABS y yi -> mul_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,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fpos0_correct _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite Fmult2_correct. clear H2. intro H2. generalize (Fle2_correct _ _ H3). rewrite Fmult2_correct. clear H3. intro H3. unfold ABS in *. split. exact H1. rewrite Rabs_mult. apply IRmult_pp with (lower xi) (upper xi) (lower yi) (upper yi) ; intuition. Qed.
imports: Gappa_common Gappa_pred_nzr