proposition: Lemma SN_iter_S : forall n x, SN (iter R n) x -> SN (iter R (S n)) x.
proof: Proof. intros. elim H. intros. apply SN_intro. intros. assert ((iter R n @ iter R 0) x0 y). apply iter_commut. hyp. do 2 destruct H3. ded (H1 _ H3). eapply SN_commut with (S := iter R 0). apply iter_commut. apply H5. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter)