fact: Fixpoint global_less_rel {T : Type} (c : LessChain T) : LessRel := match c with | base_lc _ _ (rel,_) => rel | link_ec_less _ _ (rel,_) => rel | link_lc_eq _ lc _ => global_less_rel lc | link_lc_less _ lc (rel,_) => less_relation_flow (global_less_rel lc) rel end.
imports: Reals.Rbase