proposition: Lemma iffPb (b1 b2 : bool) : reflect (b1 <-> b2) (b1 == b2).
proof: Proof. case: eqP=>[->|N]; constructor=>//. case: b1 b2 N; case=>//= _. - by case=>/(_ erefl). by case=>_ /(_ erefl). Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)