proposition: Lemma connect_rev : (connect (fun x : T => e^~ x)) =2 (fun x => (connect e)^~x).
proof: Proof. suff crev e': subrel (connect (fun x : T => e'^~ x)) (fun x => (connect e')^~x). by move=> x y; apply/idP/idP; apply: crev. move=> x y /connectP[p e_p p_y]; apply/connectP. exists (rev (belast x p)); first by rewrite p_y rev_path. by rewrite -(last_cons x) -rev_rcons p_y -lastI rev_cons last_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition