proposition: Lemma const_fun_is_lipschitz : forall b : B, lipschitz (Const_CSetoid_fun X B b).
proof: Proof. intro b. red in |- *. exists 1. intros. astepr (Two[^]1[*](x[-d]y)). astepr (Two[*](x[-d]y)). unfold Const_CSetoid_fun in |- *. rewrite -> leEq_def in |- *. red in |- *. simpl in |- *. intros H. apply (ap_irreflexive_unfolded B b). apply (ax_d_pos_imp_ap B (cms_d (c:=B)) (CPsMetricSpace_is_CPsMetricSpace B)). apply leEq_less_trans with (([0][+][1][+][1])[*](x[-d]y)). astepr ((Two:IR)[*](x[-d]y)). apply shift_leEq_mult' with (two_ap_zero IR). apply pos_two. astepl ZeroR. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. exact H. Qed.
imports: CoRN.metrics.CPseudoMSpaces