proposition: Lemma high_lowD : [predI low & high] =i pred0.
proof: Proof. case=>x; rewrite inE /low /high /= -!topredE /=. by case: x=>// n; case E: (0 %% 2 == _)=>//=; rewrite -(eqP E). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep