proposition: Lemma hombnd_add : 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. apply hombnd_plus. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)