fact: Fixpoint ec_map {A B : Type} (f : A -> B) (c : EqualChain A) : EqualChain B := match c with | base_ec _ x (rel,y) => base_ec _ (f x) (rel,f y) | link_ec_eq _ ec (rel,z) => link_ec_eq _ (ec_map f ec) (rel, f z) end.
imports: Reals.Rbase