proposition: Theorem mul_fix : forall x y : R, forall xn yn zn : Z, FIX x xn -> FIX y yn -> Zle_bool zn (xn + yn) = true -> FIX (x * y)%R zn.
proof: Proof. intros x y xn yn zn (fx,(Hx1,Hx2)) (fy,(Hy1,Hy2)) Hb. generalize (Zle_bool_imp_le _ _ Hb). clear Hb. intro H1. exists (Fmult2 fx fy). split. rewrite <- Hx1. rewrite <- Hy1. apply Fmult2_correct. apply Z.le_trans with (1 := H1). exact (Zplus_le_compat _ _ _ _ Hx2 Hy2). Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux