proposition: Lemma covers_path x y : reflect (exists2 s, path covers x s & y = last x s) (x <= y).
proof: Proof. by rewrite -covers_connect; apply: (iffP connectP). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools