proposition: Lemma hombnd_fact : forall m M1 M2 u v b B, (M1 <= M2)%R -> hombnd m M1 u v b B -> hombnd m M2 u v b B.
proof: Proof. intros m M1 M2 u v b B HM [H1 [H2 H]]. refine (conj H1 (conj H2 _)). intros H0. destruct (H H0) as [H3 H4]. split. apply Rle_trans with (1 := H3). now apply Rmult_le_compat_l. apply Rle_trans with (1 := H4). apply Rmult_le_compat_l with (2 := HM). now apply Rle_trans with (1 := Rle_0_1). Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)