proposition: Lemma prod_unitb (x : prodPCM U V) : reflect (x = Unit) (unitb x.1 && unitb x.2).
proof: Proof. case: x=>x1 x2; case: andP=>/= H; constructor. - by case: H=>/unitbP -> /unitbP ->; rewrite pcmPE. by rewrite pcmPE; case=>X1 X2; elim: H; rewrite X1 X2 !tpcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)