proposition: Lemma dsub_tri_ineq : forall (X : CPsMetricSpace) (P : cms_crr X -> CProp), tri_ineq (dsub P).
proof: Proof. intros X P. unfold tri_ineq in |- *. intros x y z. unfold dsub in |- *. case z. case y. case x. intros a H b H0 c H1. simpl in |- *. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.IR_CPMSpace