proposition: Lemma comp_cont (D1 D2 D3 : cpo) (f1 : D2 -> D1) (f2 : D3 -> D2) : continuous f1 -> continuous f2 -> continuous (f1 \o f2).
proof: Proof. case=>M1 H1 [M2 H2]; exists (comp_mono M1 M2); move=>d. by rewrite /= H2 H1 comp_chainE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)