proposition: Lemma Iter_split : forall n, Iter << iter_le n U Iter_ge (S n).
proof: Proof. induction n; simpl; intros; unfold inclusion; intros. do 2 destruct H. destruct x0. left. auto. right. exists (S x0). intuition. ded (IHn _ _ H). destruct H0. left. right. exact H0. do 2 destruct H0. case (le_lt_dec x0 (S n)); intro. assert (x0 = S n). lia. subst x0. left. left. exact H1. right. exists x0. intuition. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)