proposition: Lemma iterK n (T : Type) (f g : T -> T) : cancel f g -> cancel (iter n f) (iter n g).
proof: Proof. by move => can_fg; elim: n => // n IHn x; rewrite iterS iterSr IHn can_fg. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)