proposition: Lemma prod0cpsmetricspace_is_CPsMetricSpace : forall A B : CPsMetricSpace, is_CPsMetricSpace (ProdCSetoid A B) (d_prod0 A B).
proof: Proof. intros A B. apply (Build_is_CPsMetricSpace (ProdCSetoid A B) (d_prod0 A B)). unfold com in |- *. intros x y. unfold d_prod0 in |- *. simpl in |- *. unfold dprod0 in |- *. case x. case y. intros. apply (cs_bin_op_wd IR csg_op). apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. unfold nneg in |- *. intros. unfold d_prod0 in |- *. simpl in |- *. unfold dprod0 in |- *. case x. case y. intros. astepl (ZeroR[+][0]). apply plus_resp_leEq_both. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. unfold pos_imp_ap in |- *. intros x y. unfold d_prod0 in |- *. simpl in |- *. unfold dprod0 in |- *. case x. case y. intros c c0 c1 c2 H. unfold prod_ap in |- *. unfold prod_rect in |- *. set (H0 := positive_Sum_two IR (c1[-d]c) (c2[-d]c0) H) in *. elim H0. intros. left. apply ax_d_pos_imp_ap with (d := cms_d (c:=A)). apply CPsMetricSpace_is_CPsMetricSpace. exact a. intros. right. apply ax_d_pos_imp_ap with (d := cms_d (c:=B)). apply CPsMetricSpace_is_CPsMetricSpace. exact b. unfold tri_ineq in |- *. intros. unfold d_prod0 in |- *. simpl in |- *. unfold dprod0 in |- *. case x. case y. case z. intros c c0 c1 c2 c3 c4. astepr ((c3[-d]c1)[+]((c4[-d]c2)[+]((c1[-d]c)[+](c2[-d]c0)))). astepr ((c3[-d]c1)[+]((c4[-d]c2)[+](c1[-d]c)[+](c2[-d]c0))). astepr ((c3[-d]c1)[+]((c1[-d]c)[+](c4[-d]c2)[+](c2[-d]c0))). astepr ((c3[-d]c1)[+]((c1[-d]c)[+]((c4[-d]c2)[+](c2[-d]c0)))). astepr ((c3[-d]c1)[+](c1[-d]c)[+]((c4[-d]c2)[+](c2[-d]c0))). apply plus_resp_leEq_both. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.IR_CPMSpace