proposition: Lemma normal_compose f g: normal f -> normal g -> normal (f \o g).
proof: Proof. move => [pa pb pc][pa' pb' pc']; split. - by move => x nx; apply: pa; apply: pa'. - by move => x y nx ny h; apply: pb; [ apply: pa' | apply: pa' | apply: pb']. - move => x nx lx. move: (pa' _ nx) => ny. have lg: T3limit (g x) by apply:normal_limit. move:(pc _ ny lg) => [qa qb qc]; split => //. move => y nu yx /=; apply:T3ltW;apply: pb; auto. move: (pc' _ nx lx) => [qa' qb' qc']. move => z' nz' h /=; move: (qc _ nz' h) => [y /and3P[ya yb yc]]. move: (qc' _ ya yb) => [z /and3P[za zb zc]]; exists z. by rewrite za zb /=; apply: (T3lt_trans yc); apply: pb => //; apply: pa'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)