proposition: Lemma hombnd_cond : forall m1 m2 M u v b B, (m2 <= m1)%R -> hombnd m1 M u v b B -> hombnd m2 M u v b B.
proof: Proof. intros m1 m2 M u v b B Hm [H1 [H2 H]]. refine (conj H1 (conj H2 _)). intros H0. apply H. now apply Rle_trans with (2 := Hm). Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)