(* This file was extracted from the code provided in:
 * https://perso.ens-lyon.fr/christian.doczkal/itp18/tw2/TwoPoint.sgraph.html
 * for the sake of maintaining compatibility with unforeseen changes.
 * The original code was made by Christian Doczkal, Damien Pous and Guillaume Combette *)

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Set Bullet Behavior "Strict Subproofs".

Record sgraph := SGraph { svertex :> finType ;
                         sedge: rel svertex;
                         sg_sym: symmetric sedge;
                         sg_irrefl: irreflexive sedge}.

Notation "x -- y" := (sedge x y) (at level 30).
Definition sgP := (sg_sym,sg_irrefl).
Prenex Implicits sedge.

Lemma sg_edgeNeq (G : sgraph) (x y : G) : x -- y -> (x == y = false).
Proof. apply: contraTF => /eqP ->. by rewrite sg_irrefl. Qed.

(* The file ends here.
 * Below, some commands were added for pretty-print some symbols that can not be processed by coqdocjs *)
Notation "∅" := (set0).
Notation "x ∈ A" := (x \in A) (at level 70).
Notation "x ∉ A" := (x \notin A) (at level 70).
Notation "A ⊆ B" := (A \subset B) (at level 70, no associativity).
Notation "A ⊂ B" := (A \proper B) (at level 70, no associativity).
Notation "'Σ' ( i 'in' T ) F" := (\sum_(i in T) F) (at level 41, F at level 41, i, T at level 50).
Notation "'Σ' ( i 'in' T | P ) F" := (\sum_(i in T | P) F) (at level 41, F at level 41, i, T at level 50).
Notation "'⋃' ( i 'in' T | P ) F" := (\bigcup_(i in T | P) F) (at level 41, F at level 41, i, T at level 50).
Notation "❴ x ❵" := [set x] (at level 0, x at level 99).
Notation "❴ x | P ❵" := [set x | P] (at level 0, x, P at level 99).
Notation "❴ a1 ; a2 ; .. ; an ❵" := (setU .. (a1 |: [set a2]) .. [set an]) (at level 0, a1 at level 99).