proposition: Lemma lip_extension_strext_case: forall (x : M) (y : M) (z1 : IR) (z2 : IR) (H : z1[<]z2) (H1 : set_glb_IR (fun v : IR => sigT (fun x : subcsetoid_crr M P => f x[+]C[*]dsub' M P y x[=]v)) z1) (H2 : set_glb_IR (fun v : IR => sigT (fun x0 : subcsetoid_crr M P => f x0[+]C[*]dsub' M P x x0[=]v)) z2), x [#] y.
proof: Proof. unfold set_glb_IR. intros. destruct H1 as [l s]. destruct H2 as [l0 s0]. assert {x0 : IR | sigT (fun x1 : subcsetoid_crr M P => f x1[+]C[*]dsub' M P y x1[=]x0) | x0[-]z1[<](z2 [-] z1)}. apply s. apply shift_zero_less_minus; auto. destruct X. destruct s1. assert (z2[<=]f x1[+]C[*]dsub' M P x x1). apply (l0 (f x1[+]C[*]dsub' M P x x1)). exists x1. algebra. assert (x0 [<] z2). apply plus_cancel_less with ([--]z1). algebra. assert (f x1[+]C[*]dsub' M P y x1 [<] f x1[+]C[*]dsub' M P x x1). apply less_leEq_trans with z2; auto. astepl (x0). auto. assert ((from_SubPsMetricSpace M P x1[-d] y)[#](from_SubPsMetricSpace M P x1[-d]x)). apply less_imp_ap. apply mult_cancel_less with (z := C). apply constant_positive. astepl (C[*]dsub' M P y x1). astepr (C[*]dsub' M P x x1). apply plus_cancel_less with (f x1). astepl (f x1[+]C[*]dsub' M P y x1). astepr (f x1[+]C[*]dsub' M P x x1). auto. set (H1 := csbf_strext _ _ _ (cms_d (c:=M)) _ _ _ _ X1). elim H1. assert (Not (from_SubPsMetricSpace M P x1[#]from_SubPsMetricSpace M P x1)). apply ap_irreflexive_unfolded. contradiction. intros. apply ap_symmetric_unfolded. auto. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory