proposition: Lemma dprod0_strext : forall A B : CPsMetricSpace, bin_fun_strext (ProdCSetoid A B) (ProdCSetoid A B) IR (dprod0 A B).
proof: Proof. intros A B. unfold bin_fun_strext in |- *. intros x1 x2 y1 y2. unfold dprod0 in |- *. case x1. case x2. case y1. case y2. intros c c0 c1 c2 c3 c4 c5 c6 H. set (H1 := cs_bin_op_strext IR csg_op (c5[-d]c1) (c3[-d]c) (c6[-d]c2) (c4[-d]c0) H) in *. elim H1. intros. set (H2 := csbf_strext A A IR cms_d c5 c3 c1 c a) in *. elim H2. intros. left. simpl in |- *. left. exact a0. intros. right. simpl in |- *. left. exact b. intros. set (H2 := csbf_strext B B IR cms_d c6 c4 c2 c0 b) in *. elim H2. intros. left. simpl in |- *. right. exact a. intros. right. simpl in |- *. right. exact b0. Qed.
imports: CoRN.metrics.IR_CPMSpace