proposition: Lemma proj2_prodE : proj2_chain prod_chain = [f2 ^^ proj2_chain s by M2].
proof: Proof. rewrite /proj2_chain /prod_chain !comp_chainE !/comp /=. by apply/chainE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)