proposition: Lemma proj2_diagE : proj2_chain diag_chain = s.
proof: Proof. by rewrite /proj2_chain /diag_chain comp_chainE id_chainE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)