proposition: Lemma iter_Iter_ge : forall n p, iter n @ Iter_ge p << Iter_ge (n+p+1).
proof: Proof. unfold inclusion. intros. do 2 destruct H. do 2 destruct H0. exists (n+x1+1). intuition. apply iter_iter. exists x0. intuition. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)