proposition: Theorem Qpositive_mult_simpl : forall w w' w'' : Qpositive, Qpositive_mult w w'' = Qpositive_mult w' w'' -> w = w'.
proof: Proof. intros w w' w'' H; rewrite <- (Qpositive_mult_One w); rewrite <- (Qpositive_mult_One w'); rewrite <- (Qpositive_mult_inv w''). repeat rewrite Qpositive_mult_assoc; repeat rewrite (Qpositive_mult_sym (Qpositive_inv w'')); repeat rewrite <- Qpositive_mult_assoc. repeat rewrite (Qpositive_mult_sym w''). rewrite H; auto. Qed.