proposition: Lemma eq_dir_b_eq : forall d1 d2, eq_dir_b d1 d2 = true <-> d1 = d2.
proof: Proof. intros. unfold eq_dir_b. destruct d1; destruct d2; split; auto; intro Contra; inversion Contra. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List