proposition: Theorem Qpositive_mult_sym : forall w w' : Qpositive, Qpositive_mult w w' = Qpositive_mult w' w.
proof: Proof. intros w w'. elim (interp_non_zero w); intros p Hex; elim Hex; intros q Heq; clear Hex. elim (interp_non_zero w'); intros p' Hex; elim Hex; intros q' Heq'; clear Hex. unfold Qpositive_mult in |- *; rewrite Heq; rewrite Heq'; repeat rewrite <- (Nat.mul_comm (S p)); repeat rewrite <- (Nat.mul_comm (S q)); auto. Qed.