proposition: Lemma traces_iter_S i x: traces_iter x x i ≡ traces_iter (traces_one tt) x (S i).
proof: Proof. induction i; simpl traces_iter. symmetry. apply traces_dotx1. now apply (op_leq_weq_2 (Hf:=@traces_dot_leq _ _ _)). Qed.
imports: prop monoid positives comparisons