proposition: Lemma hombnd_cond' : forall m M u v b B, hombnd (Rmin Bmin m) M u v b B -> hombnd m M u v b B.
proof: Proof. intros m M u v b B [H1 [H2 H]]. refine (conj H1 (conj H2 _)). intros H0. apply H. apply Rmin_glb with (2 := H0). apply Rle_refl. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)