proposition: Lemma optionE (A B : Type) (o : option A) (b : B) (f : A -> B) : match o with | Some a => f a | None => b end = oapp f b o.
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching