proposition: Lemma iter_swap2 (a: X A B) b: forall n, a * iter (b*a) n == iter (a*b) n * a.
proof: Proof. induction n; simpl. rewrite dot_neutral_left. trivial with algebra. monoid_rewrite IHn. rewrite 2 dot_assoc. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(BoolView)