proposition: Theorem Qmult_assoc : forall n m p : Q, Qmult n (Qmult m p) = Qmult (Qmult n m) p.
proof: Proof. intros n m p; case p; case m; case n; auto; intros n' m' p'; simpl in |- *; rewrite Qpositive_mult_assoc; auto. Qed.