proposition: Lemma abn : forall n, a::repeat (b::nil) n == repeat (b::nil) n ++ (a::nil).
proof: Proof. induction n. - reflexivity. - simpl; transitivity (b :: a :: repeat (b :: nil) n). + repeat constructor. + now rewrite IHn. Qed.
imports: List Relation_Operators Operators_Properties Morphisms Setoid EMonoid