proposition: Lemma iffBool (b1 b2:bool) : (b1 <-> b2) -> b1==b2.
proof: Proof. destruct b1; destruct b2; intuition. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec