fact: CoInductive is_cut (X : rat -> Prop) : Prop := IsCut (ub : exists a, X a) (lb : exists a, ~ X a) (filter : forall a b, X a -> (a < b)%R -> X b) (open : forall a, X a -> exists2 b, X b & (b < a)%R).
imports: mathcomp(all_ssreflect all_algebra) Setoid