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