proposition: Lemma CSUC_connect_support : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (cont_mod : forall x:CRcarrier R, 0 < x -> CRcarrier R), CSUC f a b cont_mod -> (forall x : CRcarrier R, (sum (x <= a) (b <= x)) -> f x == 0).
proof: Proof. intros. destruct H, u. split. - intro abs. destruct H0. + apply CRopp_gt_lt_contravar in abs. rewrite CRopp_0 in abs. specialize (c1 (-f x) (x - (cont_mod (-f x) abs) * CR_of_Q R (1#2)) x abs). apply (CRle_abs (-f x)). apply (CRle_lt_trans _ (CRabs _ (f (x - cont_mod (- f x) abs * CR_of_Q R (1 # 2)) - f x))). rewrite (c (x - cont_mod (-f x) abs * CR_of_Q R (1#2))). unfold CRminus. rewrite CRplus_0_l. apply CRle_refl. left. apply (CRlt_le_trans _ (x + 0)). apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. rewrite CRplus_0_r. exact c2. apply c1. setoid_replace (x + - (cont_mod (-f x) abs * CR_of_Q R (1#2)) + - x) with (- (cont_mod (-f x) abs * CR_of_Q R (1#2))). rewrite CRabs_opp. rewrite CRabs_right. rewrite <- (CRmult_1_r (cont_mod (- f x) abs)). rewrite CRmult_assoc. apply CRmult_lt_compat_l. apply c0. rewrite CRmult_1_l. apply CR_of_Q_lt; reflexivity. apply CRlt_asym. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. + apply CRopp_gt_lt_contravar in abs. rewrite CRopp_0 in abs. specialize (c1 (-f x) (x + (cont_mod (-f x) abs) * CR_of_Q R (1#2)) x abs). apply (CRle_abs (-f x)). apply (CRle_lt_trans _ (CRabs _ (f (x + cont_mod (- f x) abs * CR_of_Q R (1 # 2)) - f x))). rewrite (c (x + cont_mod (-f x) abs * CR_of_Q R (1#2))). unfold CRminus. rewrite CRplus_0_l. apply CRle_refl. right. apply (CRle_lt_trans _ (x + 0)). rewrite CRplus_0_r. exact c2. apply CRplus_lt_compat_l. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. apply c1. setoid_replace (x + (cont_mod (-f x) abs * CR_of_Q R (1#2)) + - x) with (cont_mod (-f x) abs * CR_of_Q R (1#2)). rewrite CRabs_right. rewrite <- (CRmult_1_r (cont_mod (- f x) abs)). rewrite CRmult_assoc. apply CRmult_lt_compat_l. apply c0. rewrite CRmult_1_l. apply CR_of_Q_lt; reflexivity. apply CRlt_asym. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. - intro abs. destruct H0. + specialize (c1 (f x) (x - (cont_mod (f x) abs) * CR_of_Q R (1#2)) x abs). apply (CRle_abs (f x)). apply (CRle_lt_trans _ (CRabs _ (f (x - cont_mod (f x) abs * CR_of_Q R (1 # 2)) - f x))). rewrite (c (x - cont_mod (f x) abs * CR_of_Q R (1#2))). unfold CRminus. rewrite CRplus_0_l, CRabs_opp. apply CRle_refl. left. apply (CRlt_le_trans _ (x + 0)). apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. rewrite CRplus_0_r. exact c2. apply c1. setoid_replace (x + - (cont_mod (f x) abs * CR_of_Q R (1#2)) + - x) with (- (cont_mod (f x) abs * CR_of_Q R (1#2))). rewrite CRabs_opp. rewrite CRabs_right. rewrite <- (CRmult_1_r (cont_mod (f x) abs)). rewrite CRmult_assoc. apply CRmult_lt_compat_l. apply c0. rewrite CRmult_1_l. apply CR_of_Q_lt; reflexivity. apply CRlt_asym. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. + specialize (c1 (f x) (x + (cont_mod (f x) abs) * CR_of_Q R (1#2)) x abs). apply (CRle_abs (f x)). apply (CRle_lt_trans _ (CRabs _ (f (x + cont_mod (f x) abs * CR_of_Q R (1 # 2)) - f x))). rewrite (c (x + cont_mod (f x) abs * CR_of_Q R (1#2))). unfold CRminus. rewrite CRplus_0_l, CRabs_opp. apply CRle_refl. right. apply (CRle_lt_trans _ (x + 0)). rewrite CRplus_0_r. exact c2. apply CRplus_lt_compat_l. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. apply c1. setoid_replace (x + (cont_mod (f x) abs * CR_of_Q R (1#2)) + - x) with (cont_mod (f x) abs * CR_of_Q R (1#2)). rewrite CRabs_right. rewrite <- (CRmult_1_r (cont_mod (f x) abs)). rewrite CRmult_assoc. apply CRmult_lt_compat_l. apply c0. rewrite CRmult_1_l. apply CR_of_Q_lt; reflexivity. apply CRlt_asym. apply CRmult_lt_0_compat. apply c0. apply CR_of_Q_pos; reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal