proposition: Lemma order_le_fix m z : iter m.+1 f z = z -> order f z <= m.+1.
proof: Proof. move=> fix_z. apply: order_le_looping. by rewrite /looping fix_z trajectS mem_head. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)