fact: Definition scott_cont `{tA : t A leA} `{tB : t B leB} (f : A -> B) := forall I (g : I -> A), @directed _ leA _ g -> forall m, @sup _ leA _ g m -> @sup _ leB _ (fun i => f (g i)) (f m).
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat