proposition: Lemma hombnd_mult : forall m M1 u1 v1 b1 B1 M2 u2 v2 b2 B2, hombnd m M1 u1 v1 b1 B1 -> hombnd m M2 u2 v2 b2 B2 -> hombnd m (M1 * M2) (u1 * u2) (v1 * v2) (mult_err b1 B1 b2 B2) (Fmult B1 B2).
proof: Proof. intros m M1 u1 v1 b1 B1 M2 u2 v2 b2 B2 [H11 [H12 H1]] [H21 [H22 H2]]. unfold hombnd, mult_err. rewrite 2!F2R_plus, 4!F2R_mult. split. apply Rplus_le_le_0_compat. apply Rplus_le_le_0_compat. apply Rmult_le_pos with (1 := H11). now apply Rle_trans with (1 := Rle_0_1). apply Rmult_le_pos with (2 := H21). now apply Rle_trans with (1 := Rle_0_1). now apply Rmult_le_pos. split. rewrite <- (Rmult_1_r 1). now apply Rmult_le_compat ; try apply Rle_0_1. intros H. destruct (H1 H) as [H13 H14]. destruct (H2 H) as [H23 H24]. assert (H0: forall u v, ((u * v) * (M1 * M2) = (u * M1) * (v * M2))%R). intros u v ; ring. split. replace (u1 * u2 - v1 * v2)%R with ((u1 - v1) * v2 + v1 * (u2 - v2) + (u1 - v1) * (u2 - v2))%R by ring. rewrite 2!Rmult_plus_distr_r. rewrite 3!H0. apply Rle_trans with (1 := Rabs_triang _ _). apply Rplus_le_compat. apply Rle_trans with (1 := Rabs_triang _ _). apply Rplus_le_compat. rewrite Rabs_mult. now apply Rmult_le_compat ; try apply Rabs_pos. rewrite Rabs_mult. now apply Rmult_le_compat ; try apply Rabs_pos. rewrite Rabs_mult. now apply Rmult_le_compat ; try apply Rabs_pos. rewrite H0, Rabs_mult. now apply Rmult_le_compat ; try apply Rabs_pos. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)