proposition: Theorem rng_add_shuffle0 : ∀ n m p, (n + m + p = n + p + m)%K.
proof: Proof. intros n m p; simpl. do 2 rewrite <- rng_add_assoc. assert (m + p = p + m)%K as H by apply rng_add_comm. rewrite H; reflexivity. Qed.
imports: Utf8 Setoid