proposition: Theorem WeakConfluence_is_ChurchRosser_plus A: forall (a b : X A A), b^+ * a# <== a# * b^+ + a^+ * b# <-> (a+b)^+ <== a# * b^+ + a^+ * b#.
proof: Proof. intros a b; split; intro H. star_right_induction. rewrite (a_leq_star_a a) at 5. rewrite <- (star_make_right b) at 2. semiring_normalize. monoid_rewrite H. unfold leq. kleene_reflexivity. rewrite <- H. kleene_reflexivity. Qed.
imports: ATBR(ATBR)