fact: Definition optionR (a1 a2 : option A) := match a1, a2 with Some e1, Some e2 => R e1 e2 | None, None => True | _, _ => False end.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)