proposition: Theorem BubbleSort A: forall (a b : X A A), b * a <== a * b -> (a+b)# <== a# * b#.
proof: Proof. intros a b; intro H. star_left_induction. semiring_normalize. apply semicomm_iter_left, semicomm_iter_right in H. rewrite (a_leq_star_a b) at 2. rewrite H. kleene_reflexivity. Qed.
imports: ATBR(ATBR)