NicolasRouquette

-- A basic framework for graph theory on multidigraphs in Lean
-- and a proof that no_watershed_condition is sufficient to
-- establish that a graph has a unique sink for each vertex
--
-- I hope to give some introduction to the syntax of how Lean works here,
-- but I assume some familiarity with functions, pattern matching,
-- type theory, and proofs.
--
-- The most important thing to note is that `begin` and `end` delineate
-- sections of code in "tactic/interactive proof mode" (as opposed to