proposition: Lemma GE_prop4 E s (f := VL s): GT E s -> GL E s -> (GA E s <-> forall a b c, inc a E -> inc b E -> inc c E -> f a (f b c) = f (f a b) c).
proof: Proof. move => ti la. exact: (Bourbaki_assoc (GE_prop2 ti la)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)