proposition: Lemma UCHeaviside_cont : forall {R : ConstructiveReals} (a b : CRcarrier R) (ltab : a < b), UniformCont (UCUnitHeaviside a b ltab) (fun eps epsPos => eps * (b-a)).
proof: Proof. intros. apply UCmax. apply CRle_refl. apply UCmin. apply CRlt_asym, CRzero_lt_one. assert (0 < (b - a)). apply CRlt_minus. apply ltab. split. - intros. apply CRmult_lt_0_compat; assumption. - intros. rewrite (CRabs_morph _ ((x - y) * (CRinv R (b - a) (inr (CRlt_minus a b ltab))))). rewrite CRabs_mult. rewrite (CRabs_right (CRinv R (b - a) (inr (CRlt_minus a b ltab)))). apply (CRlt_le_trans _ (eps * (b-a) * (CRinv R (b - a) (inr (CRlt_minus a b ltab))))). apply CRmult_lt_compat_r. 2: exact H0. apply CRinv_0_lt_compat, H. rewrite CRmult_assoc, CRinv_r, CRmult_1_r. apply CRle_refl. apply CRlt_asym, CRinv_0_lt_compat, H. unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. setoid_replace (x + - a + - (y + - a)) with (x+-y). reflexivity. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm, CRopp_plus_distr. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal