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