proposition: Lemma bnd_in_P_imp_ap_zero : pred_wd _ P -> bnd_away_zero_in_P -> forall x, P x -> forall Hx, F x Hx [#] [0].
proof: Proof. intros H H0 x H1 Hx. apply bnd_imp_ap_zero with (Compact (leEq_reflexive _ x)). apply H0. red in |- *; intros x0 H2. cut (x [=] x0); intros. apply H with x; auto. inversion_clear H2; apply leEq_imp_eq; auto. split; apply leEq_reflexive. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1