proposition: Lemma GEl_prop3 E f: is_law E f -> GT E (Op E f).
proof: Proof. move => Ho; apply /setP_P => x /funI_P [z zp ->]; apply: setXp_i => //. by move/setX_P: zp => [ha hb hc]; apply:Ho. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)