proposition: Lemma contains_one_correct: forall a: regex, contains_one a = true -> a == a + 1.
proof: Proof. intros. induction a; simpl in H; fold_regex. auto with algebra. discriminate. destruct (contains_one a1). 2:discriminate. rewrite IHa1 by trivial. rewrite IHa2 by trivial. semiring_reflexivity. destruct (contains_one a1). rewrite IHa1 by trivial. semiring_reflexivity. rewrite IHa2 by trivial. semiring_reflexivity. rewrite <- star_make_left. semiring_reflexivity. discriminate. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)