proposition: Lemma GE_J_Ev E a b c: inc a E -> inc b E -> inc c E -> Vg (GE_J E) (J (J a b) c) = (J a (J b c)).
proof: Proof. move => aE bE cE. have: inc (J (J (J a b) c) (J a (J b c))) (GE_J E). by apply/GE_J_P; exists a,b,c. by move /(pr2_V(GE_J_fgraph E)); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)