proposition: Lemma joinA (x y z : lift A) : join x (join y z) = join (join x y) z.
proof: Proof. case: x y z =>[|x][|y][|z] //=; first by case: (ojoin x y). case E1: (ojoin y z)=>[v1|]. - case E2: (ojoin x y)=>[v2|]; by move: (ojoinA x y z); rewrite E1 E2 /=; move=>->. case E2: (ojoin x y)=>[v2|] //. by move: (ojoinA x y z); rewrite E1 E2 /= =><-. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)