proposition: Lemma eq_connectn (r1 r2 : rel T) : r1 =2 r2 -> connectn r1 =2 connectn r2.
proof: Proof. move=> r1Er2. elim => //= n IH y; apply: eq_big => // i. by rewrite ![_ \in _]rgraphK r1Er2. Qed.
imports: mathcomp(all_ssreflect)