proposition: Lemma boolPF (H : is_true (~~ p)) : match boolP p with | AltTrue HT => T HT | AltFalse HF => F HF end = F H.
proof: Proof. destruct boolP. - by elim: (negP H). - congr F. rewrite (Eqdep_dec.eq_proofs_unicity _ i H) //. by move=> x y; have:= Bool.bool_dec x y => -[]; [left | right]. Qed.
imports: mathcomp(all_ssreflect fingroup perm)