proposition: Lemma rev_tri_ineq' : forall a b c : X, cms_d (c:=IR_as_CPsMetricSpace) (a[-d]b) (a[-d]c)[<=]b[-d]c.
proof: Proof. simpl in |- *. unfold dIR in |- *. intros a b c. apply AbsSmall_imp_AbsIR. apply rev_tri_ineq. Qed.
imports: CoRN.metrics.ContFunctions