proposition: Lemma hlE x : high x = ~~ low x.
proof: Proof. case: x=>n; rewrite /high /low /=. elim: n=>[//|m IH]; apply: negb_inj. by rewrite negbK -modnS -IH modnS modnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep