proposition: Lemma iter_finv n x : n <= order x -> iter n finv x = iter (order x - n) f x.
proof: Proof. exact: (in1T (@iter_finv_in _ _ (in2W _) _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)