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