proposition: Lemma star_distr (a b: X A A): (a + b)# == a# * (b*a#)#.
proof: Proof. apply leq_antisym. star_left_induction. semiring_normalize. ac_rewrite (star_make_right (b*a#)). rewrite <- (star_make_right a) at 4. semiring_reflexivity. rewrite <- (star_trans (a+b)). apply dot_incr. apply star_incr. auto with algebra. rewrite <- (star_idem (a+b)). apply star_incr. rewrite <- (a_star_a_leq_star_a (a+b)). apply dot_incr. auto with algebra. apply star_incr. auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)