proposition: Lemma bnd_imp_ap_zero : forall x Hx, (I x) -> F x Hx [#] [0].
proof: Proof. intros. apply AbsIR_cancel_ap_zero. apply Greater_imp_ap. elim Hf; intros. inversion_clear b. eapply less_leEq_trans; auto. auto. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1