proposition: Lemma lhE x : low x = ~~ high x.
proof: Proof. by apply: negb_inj; rewrite negbK hlE. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep