fact: Fixpoint gc_total_statement (T : Type) `{! OrderInterpretation T} (c : GreaterChain T) : Prop := match c with | base_gc _ x (rel,y) => grtr_rel_to_pred rel x y | link_ec_grtr _ ec (rel,z) => (ec_total_statement _ ec) /\ grtr_rel_to_pred rel (ec_tail ec) z | link_gc_eq _ gc (_,z) => (gc_total_statement _ gc) /\ (gc_tail gc = z) | link_gc_grtr _ gc (rel,z) => (gc_total_statement _ gc) /\ grtr_rel_to_pred rel (gc_tail gc) z end.
imports: Reals.Rbase