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