proposition: Lemma open_interval_ext_eq: forall lb1 lb2 ub1 ub2, lb1 < ub1 -> (forall x, open_interval lb1 ub1 x <-> open_interval lb2 ub2 x) -> lb1 = lb2 /\ ub1 = ub2.
proof: Proof. intros lb1 lb2 ub1 ub2 Hord Hext. assert (Hord': lb2 < ub2) by (transitivity (middle lb1 ub1) ; apply Hext, middle_is_in_the_middle ; assumption). destruct (Rlt_le_dec lb1 lb2). destruct (Rlt_le_dec ub1 lb2). assert (Hf: ~ open_interval lb2 ub2 (middle lb1 ub1)). intro Hf ; apply Rlt_irrefl with lb2 ; transitivity (middle lb1 ub1) ; [apply Hf | transitivity ub1 ; [apply middle_is_in_the_middle |]] ; assumption. apply False_ind, Hf, Hext, middle_is_in_the_middle ; assumption. assert (Hf: ~ open_interval lb2 ub2 (middle lb1 lb2)). intro Hf ; apply Rlt_irrefl with (middle lb1 lb2) ; transitivity lb2 ; [apply middle_is_in_the_middle | apply Hf] ; assumption. apply False_ind, Hf, Hext ; split ; [| apply Rlt_le_trans with lb2] ; trivial ; apply middle_is_in_the_middle ; assumption. destruct (Rlt_le_dec lb2 lb1). destruct (Rlt_le_dec lb1 ub2). assert (Hf: ~ open_interval lb1 ub1 (middle lb2 lb1)). intro Hf ; apply Rlt_irrefl with lb1 ; transitivity (middle lb2 lb1) ; [apply Hf | apply middle_is_in_the_middle] ; assumption. apply False_ind, Hf, Hext ; split ; [| transitivity lb1] ; auto ; apply middle_is_in_the_middle ; assumption. assert (Hf: ~ open_interval lb2 ub2 (middle lb1 ub1)). intro Hf ; apply False_ind, Rlt_irrefl with ub2, Rle_lt_trans with lb1 ; [| transitivity (middle lb1 ub1) ; [apply middle_is_in_the_middle | apply Hf]] ; assumption. apply False_ind, Hf, Hext, middle_is_in_the_middle ; assumption. assert (lb_eq: lb1 = lb2) by intuition (auto with real) ; split ; trivial. destruct (Rlt_le_dec ub1 ub2). assert (Hf: ~ open_interval lb1 ub1 (middle ub1 ub2)). intro Hf ; apply Rlt_irrefl with ub1 ; transitivity (middle ub1 ub2) ; [apply middle_is_in_the_middle | apply Hf] ; assumption. apply False_ind, Hf, Hext ; rewrite <- lb_eq ; split ; [transitivity ub1 |] ; auto ; apply middle_is_in_the_middle ; assumption. destruct (Rlt_le_dec ub2 ub1). assert (Hf: ~ open_interval lb2 ub2 (middle ub2 ub1)). intro Hf ; apply Rlt_irrefl with ub2 ; transitivity (middle ub2 ub1) ; [apply middle_is_in_the_middle | apply Hf] ; assumption. apply False_ind, Hf, Hext ; rewrite lb_eq ; split ; [transitivity ub2 |] ; auto ; apply middle_is_in_the_middle ; assumption. intuition (auto with real). Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics