proposition: Lemma hombnd_minus : 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 H1 [H21 [H22 H2]]. apply hombnd_plus with (1 := H1). refine (conj H21 (conj H22 _)). intros H. destruct (H2 H) as [H23 H24]. replace (- u2 - - v2)%R with (- (u2 - v2))%R by ring. rewrite 2!Rabs_Ropp. now split. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)