proposition: Lemma symconnect_trans : transitive symconnect.
proof: Proof. move=> x y z /andP[Cyx Cxy] /andP[Cxz Czx]. by rewrite /symconnect (connect_trans Cyx) ?(connect_trans Czx). Qed.
imports: HB(structures) mathcomp(all_ssreflect)