proposition: Theorem locally_true_imp : forall P Q : R -> Prop, (forall x, P x -> Q x) -> forall x, locally_true x P -> locally_true x Q.
proof: Proof. intros P Q H x (d, (Hd, H0)). exists d. split. exact Hd. intros. apply H. apply H0. exact H1. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)