proposition: Lemma covers_connect x y : (connect covers x y) = (x <= y).
proof: Proof. apply/connectP/idP => [[s]|]. elim: s x => [x /= _ -> // |s0 s IHs] x /= /andP[/andP[/ltW ltxs0 _]]. by move => {}/IHs /[apply] /(le_trans ltxs0). move: y; apply covers_ind; last by exists [::]. move=> z y Hcovers [pth Hpath Hlast]. exists (rcons pth y); last by rewrite last_rcons. by rewrite rcons_path Hpath -Hlast andTb. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools