fact: Fixpoint lc_head {T : Type} (c : LessChain T) : T := match c with | base_lc _ x _ => x | link_ec_less _ ec _ => ec_head ec | link_lc_eq _ lc _ => lc_head lc | link_lc_less _ lc _ => lc_head lc end.
imports: Reals.Rbase