Here is a demo.
Allow rewriting with equivalence relationships.
Require Import Coq.Setoids.Setoid.
A graph is a set of vertices along with an adjacency relation.
Definition graph : Type := {V : Type & V -> V -> bool}.
Count of vertices and adjacencies.
Definition create : forall V, (V -> V -> bool) -> graph := @existT _ _.
Vertices from the graph.
Definition vertices : graph -> Type := @projT1 _ _.
Affection from the schedule.
Definition adjacent : forall g1, vertices g1 -> vertices g1 -> bool := @projT2 _ _.
The complement of the graph has the same vertices, but a negative adjacency relation.
Definition complement : graph -> graph := fun g1 => create (vertices g1) (fun v1 v2 => negb (adjacent g1 v1 v2)).
Standard materials.
Definition injective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1 x2, f1 x1 = f1 x2 -> x1 = x2. Definition surjective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1, exists x2, f1 x2 = x1. Definition bijective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => injective f1 /\ surjective f1.
Two graphs are isomorphic if there is a bijection between their vertices that preserves the adjacency.
Definition isomorphic : graph -> graph -> Prop := fun g1 g2 => exists f1, bijective f1 /\ (forall x1 x2, adjacent g1 x1 x2 = adjacent g2 (f1 x1) (f1 x2)). Infix "~" := isomorphic (at level 70).
A useful fact, the proof of which I leave to you.
Conjecture C1 : forall b1 b2, negb b1 = negb b2 <-> b1 = b2.
Your fact.
Goal forall g1 g2, g1 ~ g2 <-> complement g1 ~ complement g2. Proof.
Access to chart components.
destruct g1. destruct g2.
Replace as defined by definition.
unfold isomorphic, complement, adjacent, vertices, create, projT2, projT1.
Modifications of the first order.
firstorder.
when creating an instance.
exists x1. firstorder. rewrite C1. firstorder. exists x1. firstorder.
when creating an instance.
specialize (H0 x2 x3). rewrite C1 in H0. firstorder. Qed.
Actually, this is a formalization of graphs whose adjacency relation is decidable V -> V -> bool . In intuitionistic logic, not all graphs with a common adjacency relation V -> V -> Prop have the property you want to prove.
Instead of sticking to finite or other decidable graphs, you can also go over to classical logic or use double negation translation.