proposition: Lemma same_connect_rev : connect_sym e -> connect e =2 connect (fun x y => e y x).
proof: Proof. by move=> sym_e x y; rewrite connect_rev sym_e. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition