proposition: Lemma C0_sticking_one_pt_strong : forall f gl gr a, (forall x, x <= a -> continuity_pt gl x) -> (forall x, a <= x -> continuity_pt gr x) -> (forall x, x <= a -> f x = gl x) -> (forall x, a <= x -> f x = gr x) -> continuity f.
proof: Proof. intros f gl gr a Hl Hr Hfl Hfr x. destruct (Rtotal_order x a) as [|[]]. intros eps Heps. destruct (Hl x (Rlt_le _ _ H) eps); try assumption. destruct H0. destruct (Rlt_dec x0 (a - x)). exists x0; split; try assumption. intro. destruct (Rlt_dec a x1). intros. assert False; try contradiction. apply (Rgt_asym a x1); try assumption. destruct H2; simpl in H3; unfold R_dist in H3. assert ((x1 - x) <= Rabs (x1 - x)) by apply RRle_abs. lra. repeat rewrite Hfl. apply (H1 x1). lra. apply Rnot_lt_le; assumption. apply Rnot_lt_le in n. exists (a - x); split; try lra. intro. destruct (Rlt_dec a x1). intros. assert False; try contradiction. apply (Rgt_asym a x1); try assumption. destruct H2; simpl in H3; unfold R_dist in H3. assert ((x1 - x) <= Rabs (x1 - x)) by apply RRle_abs. lra. assert (D_x no_cond x x1 /\ dist R_met x1 x < x0 -> dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)). apply Rnot_lt_le in n0. repeat rewrite Hfl; try lra. intros; destruct H3. apply H2. split; try assumption. lra. intros eps Heps. rewrite H in |-*; clear H x. destruct (Hl a (Rle_refl a) eps); try assumption. destruct (Hr a (Rle_refl a) eps); try assumption. destruct H; destruct H0. exists (Rmin x x0); split. apply Rmin_pos; assumption. intro x1; destruct (Rlt_dec x1 a). repeat rewrite Hfl; try lra. assert (D_x no_cond a x1 /\ dist R_met x1 a < x -> dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)). intros; destruct H4. apply H3. split; try assumption. assert (Rmin x x0 <= x) by exact (Rmin_l x x0). lra. apply Rnot_lt_le in n. repeat rewrite Hfr; try lra. assert (D_x no_cond a x1 /\ dist R_met x1 a < x0 -> dist R_met (gr x1) (gr a) < eps) by (exact (H2 x1)). intros; destruct H4. apply H3. split; try assumption. assert (Rmin x x0 <= x0) by exact (Rmin_r x x0). lra. intros eps Heps. destruct (Hr x (Rlt_le _ _ H) eps); try assumption. destruct H0. destruct (Rlt_dec x0 (x - a)). exists x0; split; try assumption. intro. destruct (Rlt_dec x1 a). intros. assert False; try contradiction. apply (Rgt_asym a x1); try assumption. destruct H2; simpl in H3; unfold R_dist in H3. assert (x - x1 <= Rabs (x1 - x)). rewrite Rabs_minus_sym; apply RRle_abs. lra. repeat rewrite Hfr. apply (H1 x1). lra. apply Rnot_lt_le; assumption. exists (x - a); split; try lra. intro. destruct (Rlt_dec x1 a). intros. assert False; try contradiction. apply (Rgt_asym a x1); try assumption. destruct H2; simpl in H3; unfold R_dist in H3. assert (x - x1 <= Rabs (x1 - x)). rewrite Rabs_minus_sym; apply RRle_abs. lra. apply Rnot_lt_le in n0. repeat rewrite Hfr; try lra. apply Rnot_lt_le in n. assert (D_x no_cond x x1 /\ dist R_met x1 x < x0 -> dist R_met (gr x1) (gr x) < eps) by (exact (H1 x1)). intros; destruct H3. apply H2. split; auto. lra. Qed.
imports: Reals Lra Rfunctions