proposition: Lemma hombnd_plus : forall m M u1 v1 b1 B1 u2 v2 b2 B2, hombnd m M u1 v1 b1 B1 -> hombnd m M u2 v2 b2 B2 -> hombnd m M (u1 + u2) (v1 + v2) (Fplus b1 b2) (Fplus B1 B2).
proof: Proof. intros m M u1 v1 b1 B1 u2 v2 b2 B2 [H11 [H12 H1]] [H21 [H22 H2]]. unfold hombnd. rewrite F2R_plus. split. now apply Rplus_le_le_0_compat. rewrite F2R_plus. split. clear -H12 H22 ; lra. intros H. destruct (H1 H) as [H13 H14]. destruct (H2 H) as [H23 H24]. rewrite 2!Rmult_plus_distr_r. replace ((u1 + u2) - (v1 + v2))%R with ((u1 - v1) + (u2 - v2))%R by ring. split ; apply Rle_trans with (1 := Rabs_triang _ _) ; now apply Rplus_le_compat. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)