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