proposition: Lemma GEl_prop4 E f: is_law E f -> GL E (Op E f).
proof: Proof. move => H; split => a b ha hb. exists (f a b). have ->: (f a b) = f (P (J a b)) (Q (J a b)) by aw. rewrite /Op; apply: Lg_i; fprops. move/funI_P:ha => [z ze ->]. by move/funI_P:hb => [z' ze' ->]; aw => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)