proposition: Theorem Rnd_UP_pt_equiv_format : forall F1 F2 : R -> Prop, forall a b : R, F1 b -> ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) -> forall x f, a <= x <= b -> Rnd_UP_pt F1 x f -> Rnd_UP_pt F2 x f.
proof: Proof. intros F1 F2 a b Hb HF x f Hx (H1, (H2, H3)). split. apply -> HF. exact H1. split. now apply Rle_trans with (2 := H2). now apply H3. split. exact H2. intros k Hk Hl. destruct (Rle_or_lt k b) as [H|H]. apply H3. apply <- HF. exact Hk. split. now apply Rle_trans with (2 := Hl). exact H. exact Hl. apply Rlt_le. apply Rle_lt_trans with (2 := H). now apply H3. Qed.
imports: Coq(Reals) Raux Defs