proposition: Theorem Pos_mul_shuffle0 : ∀ n m p, n * m * p = n * p * m.
proof: Proof. intros n m p. rewrite <- Pos.mul_assoc. remember (m * p) as mp. rewrite Pos.mul_comm in Heqmp; subst mp. apply Pos.mul_assoc. Qed.
imports: Utf8 QArith NPeano Sorted Psatz