proposition: Lemma connect_sym (D : finType) (r : rel D) : symmetric r -> connect_sym r.
proof: Proof. move=> ?; rewrite /connect_sym => ? ?; apply/idP/idP => /connect_sym1; exact. Qed.
imports: mathcomp(all_ssreflect fingroup perm)