proposition: Proposition maximal_indsysP p D : hereditary p -> reflect (p D /\ forall v : T, v \notin D -> ~~ p (v |: D)) (maxset p D).
proof: Proof. move/hereditaryP => p_hereditary; apply: (iffP maxset_properP). - case => pD maxD; split => // v vD. apply: maxD. by rewrite setUC properUl // sub1set. - case => pD max1D; split => // A /properP [subA [v vA /max1D vD]]. apply: contraNN vD; apply: p_hereditary; by rewrite subUset sub1set vA. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)