proposition: Lemma fconnect_invariant (T' : eqType) (k : T -> T') : invariant f k =1 xpredT -> forall x y, fconnect f x y -> k x = k y.
proof: Proof. move=> eq_k_f x y /iter_findex <-; elim: {y}(findex x y) => //= n ->. by rewrite (eqP (eq_k_f _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)