proposition: Lemma iter_com : forall a i, iter (f a) f i = f (iter a f i).
proof: Proof. induction i; simpl; intros. refl. rewrite IHi. refl. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)