proposition: Theorem locally_true_and : forall P Q x, locally_true x P -> locally_true x Q -> locally_true x (fun x => P x /\ Q x).
proof: Proof. intros P Q x HP HQ. destruct HP as (e1, (He1, H3)). destruct HQ as (e2, (He2, H4)). exists (Rmin e1 e2). split. apply Rmin_pos ; assumption. intros. split. apply H3. apply Rlt_le_trans with (1 := H). apply Rmin_l. apply H4. apply Rlt_le_trans with (1 := H). apply Rmin_r. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)