proposition: Lemma iter_iter : forall p q, iter p @ iter q << iter (p+q+1).
proof: Proof. induction p; simpl; intros. rewrite plus_1_S. simpl. refl. assoc. comp. apply IHp. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)