proposition: Lemma lip_extension_strext : fun_strext (lip_extension_f).
proof: Proof. unfold fun_strext. unfold lip_extension_f. intros x y. elim inf_f_multi_ext_exists. elim inf_f_multi_ext_exists. simpl. intros z1 H1 z2 H2 H. elim (ap_imp_less IR z1 z2); auto; intros. unfold f_multi_ext. apply (lip_extension_strext_case x y z1 z2 a H1 H2). apply ap_symmetric_unfolded. apply (lip_extension_strext_case y x z2 z1 b H2 H1). apply ap_symmetric_unfolded. auto. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory