proposition: Lemma iter_looping m z y : (forall n, n < m -> iter n f z != y) -> looping f z m -> ~~ fconnect f z y.
proof: Proof. move => not_y ?; rewrite fconnect_orbit; apply/trajectP => -[k k_lt_o]. apply/eqP; rewrite eq_sym not_y //. exact: leq_trans k_lt_o (order_le_looping _). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)