proposition: Lemma iter_split (a: X A A): forall m n, iter a (m+n) == iter a m * iter a n.
proof: Proof. induction m; intro n; simpl. auto with algebra. rewrite IHm. auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(BoolView)