proposition: Lemma zero_fun_tri_ineq : forall X : CSetoid, tri_ineq (Zero_fun X).
proof: Proof. intro X. unfold tri_ineq in |- *. intros x y z. unfold Zero_fun in |- *. simpl in |- *. unfold zero_fun in |- *. apply eq_imp_leEq. rational. Qed.
imports: CoRN.reals.Intervals