proposition: Lemma derive_pt_open_interval_id : forall a b x pr, open_interval a b x -> (derive_pt_in (open_interval a b) id x pr = 1)%R.
proof: Proof. intros a b x pr x_in ; rewrite derive_open_interval_pt with (pr' := derivable_pt_id x). apply derive_pt_id. assumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts