proposition: Lemma comp_chainE : [f1 ^^ [f2 ^^ s by M2] by M1] = [f1 \o f2 ^^ s by comp_mono].
proof: Proof. apply/chainE=>x1; split; first by case=>x2 [->][x3][->]; exists x3. by case=>x3 [->]; exists (f2 x3); split=>//; exists x3. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)