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