proposition: Lemma continuous_comp f g x: continuous_at f x -> continuous_at g (f x) -> continuous_at (g \o f) x.
proof: Proof. move => ca cb e ep; move:(cb _ ep) => [d dp dv]. move:(ca _ dp) => [e2 e2p e2v]; ex_tac => y ya /=. by apply: dv; apply: e2v. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)