proposition: Theorem mul_flt : forall x y : R, forall xn yn zn : positive, FLT x xn -> FLT y yn -> Zle_bool (Zpos (if xn =? 1 then yn else if yn =? 1 then xn else xn + yn)%positive) (Zpos zn) = true -> FLT (x * y)%R zn.
proof: Proof. intros x y xn yn zn Hx Hy Hb. apply Zle_bool_imp_le in Hb. revert Hb. apply flt_le. case Pos.eqb_spec. intros ->. now apply flt_1_aux. intros _. case Pos.eqb_spec. intros ->. rewrite Rmult_comm. now apply flt_1_aux. intros _. destruct Hx as [fx [Hx1 Hx2]]. destruct Hy as [fy [Hy1 Hy2]]. exists (Fmult2 fx fy). split. rewrite <- Hx1. rewrite <- Hy1. apply Fmult2_correct. change (Z.pow_pos 2 (xn + yn)) with (Zpower radix2 (Zpos xn + Zpos yn)). rewrite Zpower_plus by easy. simpl Z.abs. rewrite Zabs_Zmult. apply Zmult_lt_compat ; split ; try assumption ; apply Zabs_pos. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux