proposition: Lemma orrAb r1 r2 : r1 <~> r1 +p r2 <-> r2 ~> r1.
proof: Proof. split; first by move=>-> x /=; auto. move=>H x /=; split; first by auto. by case=>//; move/H. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)