proposition: Lemma dense_open_interval: forall lb ub x, lb < ub -> interval lb ub x -> dense (open_interval lb ub) x.
proof: Proof. intros lb ub x Hlt [xlb xub] eps eps_pos ; assert (lbub : 0 < ub - lb) by lra. destruct xlb as [xlb | xeq]. destruct xub as [xub | xeq]. assert (d_pos : 0 < interval_dist lb ub x / 2). apply Rlt_mult_inv_pos ; [apply open_interval_dist_pos | lra]. split ; assumption. pose (h := Rmin (eps / 2) (interval_dist lb ub x / 2)) ; assert (h_pos : 0 < h) by (apply Rmin_pos_lt ; lra). exists (x + h) ; split. split. apply open_interval_dist_bound ; [split ; left ; assumption |]. apply Rle_lt_trans with (interval_dist lb ub x / 2). rewrite Rabs_right ; [apply Rmin_r | left ; assumption]. lra. apply Rplus_pos_neq ; assumption. rewrite R_dist_Rplus_compat, Rabs_right ; [| left ; assumption]. apply Rle_lt_trans with (eps / 2) ; [apply Rmin_l | lra]. pose (h := Rmin (eps / 2) ((ub - lb) / 2)) ; assert (h_pos : 0 < h) by (apply Rmin_pos_lt ; [| apply Rlt_mult_inv_pos] ; lra). exists (x - h) ; repeat split. apply Rle_lt_trans with (x - (ub - lb)). right ; subst ; ring. apply Rplus_lt_compat_l, Ropp_lt_contravar. apply Rle_lt_trans with ((ub - lb) / 2) ; [apply Rmin_r | apply Rlt_div_2 ; assumption]. subst ; apply Rminus_pos_lt ; assumption. subst ; apply Rgt_not_eq, Rminus_pos_lt ; assumption. rewrite R_dist_Rminus_compat, Rabs_right ; [| left ; assumption]. apply Rle_lt_trans with (eps / 2) ; [apply Rmin_l | lra]. pose (h := Rmin (eps / 2) ((ub - lb)/2)) ; assert (h_pos : 0 < h) by (apply Rmin_pos_lt ; [| apply Rlt_mult_inv_pos] ; lra). exists (x + h) ; repeat split. rewrite xeq ; apply Rplus_pos_lt ; assumption. apply Rlt_le_trans with (x + (ub - lb)) ; [| right ; rewrite xeq ; ring]. apply Rplus_lt_compat_l, Rle_lt_trans with ((ub - lb)/2) ; [apply Rmin_r |]. apply Rlt_div_2 ; assumption. apply Rlt_not_eq, Rplus_pos_lt ; assumption. rewrite R_dist_Rplus_compat, Rabs_right ; [| left ; assumption]. apply Rle_lt_trans with (eps / 2) ; [apply Rmin_l | lra]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra