proposition: Lemma order_le_looping m z : looping f z m -> order f z <= m.
proof: Proof. apply: contraTT; rewrite -ltnNge -looping_uniq => m_lt_o. rewrite -(take_traject _ _ m_lt_o); exact: take_uniq (orbit_uniq _ _). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)