proposition: Lemma GE_I_fgraph E : fgraph (GE_I E).
proof: Proof. split; first by move => x /GE_I_incP []. move => x y /GE_I_incP [ha hb hc] /GE_I_incP [ha' hb' hc'] sp. by rewrite - ha -ha' -hb -hb' sp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)