proposition: Theorem Qpositive_plus_sym : forall w w' : Qpositive, Qpositive_plus w w' = Qpositive_plus 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_plus in |- *. rewrite Heq; rewrite Heq'. repeat rewrite (Nat.mul_comm (S q')). repeat rewrite (Nat.mul_comm (S p')). repeat rewrite (Nat.add_comm (S p * S q')). auto. Qed.