proposition: Lemma iter_commut : forall p q, iter p @ iter q << iter q @ iter p.
proof: Proof. intros. incl_trans (iter (p+q+1)). apply iter_iter. assert (p+q+1 = q+p+1). lia. rewrite H. apply iter_plus_1. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)