proposition: Lemma metric_d_strext : forall X : CPsMetricSpace, bin_fun_strext (Metric_CSetoid X) (Metric_CSetoid X) IR (metric_d X).
proof: Proof. intro X. unfold bin_fun_strext in |- *. intros x1 x2 y1 y2. simpl in |- *. unfold metric_d in |- *. unfold metric_ap in |- *. intro H. apply positive_Sum_two. set (H0 := less_conf_ap IR (x1[-d]y1) (x2[-d]y2)) in *. elim H0. intros H1 H2. set (H4 := H1 H) in *. elim H4. intro H5. astepr ((x1[-d]x2)[+](y1[-d]y2)[+][0]). astepr ((x1[-d]x2)[+](y1[-d]y2)[+]((x1[-d]y1)[-](x1[-d]y1))). astepr ((x1[-d]x2)[+](y1[-d]y2)[+](x1[-d]y1)[-](x1[-d]y1)). apply shift_less_minus. astepl (x1[-d]y1). apply less_leEq_trans with (x2[-d]y2). exact H5. apply leEq_transitive with ((x2[-d]x1)[+](x1[-d]y2)). apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. astepr ((x2[-d]x1)[+](y1[-d]y2)[+](x1[-d]y1)). astepr ((x2[-d]x1)[+]((y1[-d]y2)[+](x1[-d]y1))). apply plus_resp_leEq_lft. astepr ((x1[-d]y1)[+](y1[-d]y2)). apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. astepl ((y1[-d]y2)[+](x2[-d]x1)[+](x1[-d]y1)). astepr ((y1[-d]y2)[+](x1[-d]x2)[+](x1[-d]y1)). astepl ((y1[-d]y2)[+]((x2[-d]x1)[+](x1[-d]y1))). astepr ((y1[-d]y2)[+]((x1[-d]x2)[+](x1[-d]y1))). astepl ((y1[-d]y2)[+]((x1[-d]y1)[+](x2[-d]x1))). astepr ((y1[-d]y2)[+]((x1[-d]y1)[+](x1[-d]x2))). astepl ((y1[-d]y2)[+](x1[-d]y1)[+](x2[-d]x1)). astepr ((y1[-d]y2)[+](x1[-d]y1)[+](x1[-d]x2)). apply plus_resp_eq. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. intro H5. astepr ((x1[-d]x2)[+](y1[-d]y2)[+][0]). astepr ((x1[-d]x2)[+](y1[-d]y2)[+]((x2[-d]y2)[-](x2[-d]y2))). astepr ((x1[-d]x2)[+](y1[-d]y2)[+](x2[-d]y2)[-](x2[-d]y2)). apply shift_less_minus. astepl (x2[-d]y2). apply less_leEq_trans with (x1[-d]y1). exact H5. apply leEq_transitive with ((x1[-d]x2)[+](x2[-d]y1)). apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. astepr ((x1[-d]x2)[+](y1[-d]y2)[+](x2[-d]y2)). astepr ((x1[-d]x2)[+]((y1[-d]y2)[+](x2[-d]y2))). apply plus_resp_leEq_lft. astepr ((x2[-d]y2)[+](y1[-d]y2)). astepr ((x2[-d]y2)[+](y2[-d]y1)). apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. apply plus_resp_eq. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv