proposition: Lemma GE_prop3 E s (f := VL s) : GT E s -> GL E s -> is_law E f /\ (Op E f) = s.
proof: Proof. move => type l1. have ll:= (GE_prop2 type l1). have ha: is_law E f by move => x y xE yE; apply: Law_range. split => //; apply: fgraph_exten. - rewrite/Op; fprops. - by case:ll. - case:ll => _ _ ->; rewrite /Op; aw; trivial. - by rewrite /Op /f /VL Lgd => x xp; rewrite LgV// (setX_pair xp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)