proposition: Lemma same_fconnect_finv : fconnect finv =2 fconnect f.
proof: Proof. move=> x y; rewrite (same_connect_rev symf); apply: {x y}eq_connect => x y /=. by rewrite (canF_eq finv_f) eq_sym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)