proposition: Lemma dIR_apdiag_grzero : apdiag_imp_grzero IR_as_CPsMetricSpace (cms_d (c:=IR_as_CPsMetricSpace)).
proof: Proof. unfold apdiag_imp_grzero in |- *. intros x y. simpl in |- *. unfold dIR in |- *. intro H. set (H0 := AbsIR_pos) in *. generalize H0. simpl in |- *. intro H1. apply H1. apply minus_ap_zero. exact H. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv