proposition: Lemma GE_prop5 E s : GT E s -> GL E s -> GU E s -> exists2 z, inc z E & unit E s z.
proof: Proof. move => type law [z ha hb]; exists z => // a aE. pose w := (GE_prop2 type law). move:(hb _ aE) => [r1 r2]. by rewrite /unit -(Law_val w r1) -(Law_val w r2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)