proposition: Lemma red_iter : forall R : relation A, (forall x y, R x y -> R (f x) (f y)) -> forall i x y, R x y -> R (iter x f i) (iter y f i).
proof: Proof. induction i; simpl; intros. hyp. apply H. apply IHi. hyp. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)