proposition: Lemma connect_rev (g : rel V) : connect g =2 (fun x => connect (fun x => g^~ x) ^~ x).
proof: Proof. move=> x y; apply/connectP/connectP=> [] [p gp ->]; [exists (rev (belast x p))|exists (rev (belast y p))]; rewrite ?rev_path //; by case: (lastP p) => //= ??; rewrite belast_rcons rev_cons last_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect)