proposition: Lemma iter_swap (a: X A A): forall n, a * iter a n == iter a n * a.
proof: Proof. intros until n. rewrite <- (iter_once a) at 4. rewrite <- iter_split. rewrite Nat.add_comm. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(BoolView)