proposition: Lemma star_remove: forall a: regex, remove a # == a #.
proof: Proof. induction a; simpl; fold_regex; auto with algebra. case_eq (contains_one a1); intro Ha1; trivial. case_eq (contains_one a2); intro Ha2; trivial. rewrite star_plus_but_one. rewrite star_plus_star. rewrite IHa1, IHa2. rewrite <- star_plus_star. apply star_plus_star_dot; assumption. case (contains_one a1 ||| contains_one a2); trivial. rewrite star_plus_but_one. rewrite star_plus_star. rewrite IHa1, IHa2. symmetry. apply star_plus_star. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)