proposition: Lemma Bourbaki_assoc s E : Law s E -> ( (s \cg (Sprod s (GE_I E))) = ((s \cg (Sprod (GE_I E) s)) \cg (GE_J E)) <-> forall a b c, inc a E -> inc b E -> inc c E -> VL s a (VL s b c) = VL s (VL s a b) c).
proof: Proof. move => h; split. move => h1 a b c aE bE cE. have: inc (J (J (J a b) c) (VL s (VL s a b) c)) (s \cg Sprod s (GE_I E)). by apply/(Sprod_case_l1 _ h); exists a,b,c. rewrite h1;move/(Sprod_case_l2 _ h) =>[a' [b' [c' [_ _ _ ea]]]]. rewrite (pr2_def ea); move: (pr1_def ea) => eb. rewrite (pr2_def eb); move: (pr1_def eb) => ec. by rewrite (pr1_def ec) (pr2_def ec). move => h'; apply:extensionality => x. move/(Sprod_case_l1 _ h) => [a [b [c [aE bE cE ->]]]]. by rewrite - h' //; apply/(Sprod_case_l2 _ h); exists a,b,c. move/(Sprod_case_l2 _ h) => [a [b [c [aE bE cE ->]]]]. by rewrite h' //; apply/(Sprod_case_l1 _ h); exists a,b,c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)