proposition: Lemma GE_prop2_stable E s : GT E s -> GL E s -> forall a b, inc a E -> inc b E -> inc (VL s a b) E.
proof: Proof. move => ha hb; move: (GE_prop2 ha hb) => hc. move => a b aE bE. exact:(Law_range hc aE bE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)