proposition: Lemma GE_J_fgraph E : fgraph (GE_J E).
proof: Proof. split; first by move => x /GE_J_P [a [b [c [_ _ _ ->]]]]; fprops. move => x y /GE_J_P [a [b [c [_ _ _ ->]]]]/GE_J_P [a' [b' [c' [_ _ _ ->]]]]. by aw => ea;rewrite (pr2_def ea) (pr1_def (pr1_def ea)) (pr2_def (pr1_def ea)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)