proposition: Lemma altF (px : ~~ p x) : match boolP (p x) with AltTrue b => fT b | AltFalse b => fF b end = fF px.
proof: Proof. case: {-}_ /boolP => -px'; first by case:notF; rewrite px' in px. by rewrite (bool_irrelevance px' px). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)