theorem SimpleGraph.exists_orientation_of_average_degree_le {V : Type u_1} [Finite V] {G : SimpleGraph V} {d : ℕ} (hGcolorable : G.Colorable 2) (hGdeg : ∀ (s : Finset V), (induce (↑s) G).edgeSet.ncard ≤ d * s.card) : ∃ (r : V → V → Prop), Irreflexive r ∧ Std.Asymm r

A bipartite simple graph whose induced subgraphs all have average degree at most 2 * d can be oriented in such a way that all edges have outdegree at most d.