proposition: Lemma orrAb (r1 a : Pred T) : r1 <~> r1 +p a <-> a ~> r1.
proof: Proof. split; first by move=>-> x /=; auto. move=>H x /=; split; first by auto. by case=>//; move/H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool seq) Setoid