proposition: Lemma joinA x y z : ojoin x (ojoin y z) = ojoin (ojoin x y) z.
proof: Proof. by case: x; case: y; case: z=>//=c b a; rewrite joinA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)