fact: Fixpoint lc_total_statement (T : Type) `{! OrderInterpretation T} (c : LessChain T) : Prop := match c with | base_lc _ x (rel,y) => less_rel_to_pred rel x y | link_ec_less _ ec (rel,z) => (ec_total_statement _ ec) /\ less_rel_to_pred rel (ec_tail ec) z | link_lc_eq _ lc (_,z) => (lc_total_statement _ lc) /\ (lc_tail lc = z) | link_lc_less _ lc (rel,z) => (lc_total_statement _ lc) /\ less_rel_to_pred rel (lc_tail lc) z end.
imports: Reals.Rbase