proposition: Lemma nonneg_edges_to_path : forall g, nonneg_edges g -> forall x y, value_nonneg weight (is_path g x y).
proof: Proof. Proof using. introv NG H. induction H. rewrite weight_nil. math. rewrite weight_cons. forwards: NG H0. math. Qed.
imports: TLC(LibCore LibSet)