proposition: Lemma st_hereditary : hereditary stable.
proof: Proof. apply/hereditaryP. move=> D F FsubD /stableP Dstable. apply/stableP => u v uinF vinF. move: (subsetP FsubD u uinF) => uinD. move: (subsetP FsubD v vinF) => vinD. exact: Dstable. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)