proposition: Lemma relU_sym e e' : connect_sym e -> connect_sym e' -> connect_sym (relU e e').
proof: Proof. move=> sym_e sym_e'; apply: symmetric_from_pre => x _ /connectP[p e_p ->]. elim: p x e_p => //= y p IHp x /andP[e_xy /IHp{IHp}/connect_trans]; apply. case/orP: e_xy => /connect1; rewrite (sym_e, sym_e'); by apply: connect_sub y x => x y e_xy; rewrite connect1 //= e_xy ?orbT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)