fact: Fixpoint gc_head {T : Type} (c : GreaterChain T) : T := match c with | base_gc _ x _ => x | link_ec_grtr _ ec _ => ec_head ec | link_gc_eq _ gc _ => gc_head gc | link_gc_grtr _ gc _ => gc_head gc end.
imports: Reals.Rbase