proposition: Theorem rng_mul_shuffle0 : ∀ n m p, (n * m * p = n * p * m)%K.
proof: Proof. intros n m p. do 2 rewrite <- rng_mul_assoc. assert (m * p = p * m)%K as H by apply rng_mul_comm. rewrite H; reflexivity. Qed.
imports: Utf8 Setoid