proposition: Theorem mul_rr : forall x1 x2 y1 y2 : R, forall xi yi zi : FF, REL x1 x2 xi -> REL y1 y2 yi -> mul_rr_helper xi yi zi = true -> REL (x1 * y1) (x2 * y2) zi.
proof: Proof. intros x1 x2 y1 y2 xi yi zi (xe,(Hx1,Hx2)) (ye,(Hy1,Hy2)) 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). apply Fle2_m1_correct in H1. apply Fle2_m1_correct in H2. generalize (Fle2_correct _ _ H3). repeat rewrite Fplus2_correct. rewrite Fmult2_correct. clear H3. intro H3. generalize (Fle2_correct _ _ H4). repeat rewrite Fplus2_correct. rewrite Fmult2_correct. clear H4. intro H4. exists (xe + ye + xe * ye)%R. split. apply IRcompose with (1 := H1) (2 := H2) (3 := H3) (4 := H4) (5 := Hx1) (6 := Hy1). rewrite Hx2. rewrite Hy2. ring. Qed.
imports: Gappa_common Gappa_pred_bnd