proposition: Lemma extend_continuously_extends_interval : forall a b f x, Rinterval.interval a b x -> f x = extend_continuously f a b x.
proof: Proof. intros a b f x [alex xleb] ; unfold extend_continuously. destruct (Rlt_le_dec x a). + destruct (Rlt_irrefl x) ; apply Rlt_le_trans with a ; assumption. + destruct (Rle_lt_dec x b). - reflexivity. - destruct (Rlt_irrefl x) ; apply Rle_lt_trans with b ; assumption. Qed.
imports: Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Rbase MyRIneq MyR_dist Rfunctions Lra