feat(combinatorics/simple_graph/basic): add decidable instance for ad…

…jacency of complement (#6000)

Add instance that states that, if the adjacency relation for a simple graph is decidable, the adjacency relation for its complement is also decidable. 



Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>

src/combinatorics/simple_graph/basic.lean

@@ -442,6 +442,9 @@ instance has_compl : has_compl (simple_graph V) :=
 @[simp]
 lemma compl_adj (G : simple_graph V) (v w : V) : Gᶜ.adj v w ↔ v ≠ w ∧ ¬G.adj v w := iff.rfl
 
+instance compl_adj_decidable (V : Type u) [decidable_eq V] (G : simple_graph V)
+  [decidable_rel G.adj] : decidable_rel Gᶜ.adj := λ v w, and.decidable
+
 @[simp]
 lemma compl_compl (G : simple_graph V) : Gᶜᶜ = G :=
 begin