proposition: Lemma noid_prop5g y i j k: gle r i j -> gle r j k -> inc y (Vg E i) -> Vf (Vg f (J j k)) (Vf (Vg f (J i j)) y) = Vf (Vg f (J i k)) y.
proof: Proof. move => lij ljk yEi. move:(function_f lij)(function_f ljk); aw; move =>[fa sa ta][fb sb tb]. have cop:Vg f (J j k) \coP Vg f (J i j) by split => //; ue. move:(f_equal (Vf^~ y) (compose_f lij ljk)); rewrite compfV //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)