fact: Definition eq_dir_b (d1 d2 : SplitDirection) : bool := match d1,d2 with | Left, Left => true | Right, Right => true | _, _ => false end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List