proposition: Lemma star_plus_star_dot: forall a b: regex, contains_one a = true -> contains_one b = true -> (a+b)# == (a*b)#.
proof: Proof. intros. rewrite (contains_one_correct a), (contains_one_correct b); trivial. apply leq_antisym. apply star_incr. semiring_reflexivity. apply star_dot_leq_star_plus. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)