proposition: Lemma FImult2_correct : forall (x : float2) yi y, BND y yi -> BND (x * y) (FImult2 x yi).
proof: Proof. intros x (yl,yu) y Hy. unfold FImult2. replace (Fpos0 x) with (Zle_bool 0 (Fnum x)) by now unfold Fpos0 ; case (Fnum x). case Zle_bool_spec ; split ; simpl ; rewrite Fmult2_correct. apply monotony_1p. now apply Float_prop.F2R_ge_0. apply Hy. apply monotony_1p. now apply Float_prop.F2R_ge_0. apply Hy. apply monotony_1n. apply Float_prop.F2R_le_0. now apply Zlt_le_weak. apply Hy. apply monotony_1n. apply Float_prop.F2R_le_0. now apply Zlt_le_weak. apply Hy. Qed.
imports: Gappa_common Gappa_pred_bnd