proposition: Lemma connected_mirror : connected mirror = connected G.
proof: Proof. by rewrite /connected (eq_n_comp gcomp_mirror). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)