proposition: Lemma pathb_correct l : pathb l = true <-> path l.
proof: Proof. induction l as [ | [x y] [ | [y' z] l] IHl ]. - split; constructor. - split; constructor. - change (pathb ((x, y) :: (y', z) :: l)) with ((y =? y') && pathb ((y', z) :: l))%bool. destruct (y =? y') eqn:E. + rewrite Bool.andb_true_l. rewrite IHl. apply Nat.eqb_eq in E. subst y'. split. * constructor; auto. * intros H; inversion H; auto. + simpl. split. discriminate. apply Nat.eqb_neq in E. intros H; inversion H; auto. Qed.
imports: Arith List Permutation