proposition: Lemma extension_C0_ext (f : R -> V) (a b : Rbar) : forall (x : R), Rbar_le a x -> Rbar_le x b -> (extension_C0 f a b) x = f x.
proof: Proof. move => x Hax Hxb. rewrite /extension_C0. case: Rbar_le_dec => // _. case: Rbar_le_dec => // _. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv