fact: Fixpoint global_grtr_rel {T : Type} (c : GreaterChain T) : GreaterRel := match c with | base_gc _ _ (rel,_) => rel | link_ec_grtr _ _ (rel,_) => rel | link_gc_eq _ gc _ => global_grtr_rel gc | link_gc_grtr _ gc (rel,_) => grtr_relation_flow (global_grtr_rel gc) rel end.
imports: Reals.Rbase