proposition: Lemma existsb_tnth a t : [exists i, a (tnth t i)] = has a t.
proof: Proof. by apply: negb_inj; rewrite negb_exists -all_predC -forallb_tnth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)