proposition: Lemma zero_fun_pos_imp_ap : forall X : CSetoid, pos_imp_ap (Zero_fun X).
proof: Proof. intro X. unfold pos_imp_ap in |- *. intros x y. unfold Zero_fun in |- *. simpl in |- *. unfold zero_fun in |- *. intro Z. set (H := less_irreflexive IR [0] Z) in *. intuition. Qed.
imports: CoRN.reals.Intervals