proposition: Theorem Qpositive_plus_simpl : forall w w' w'' : Qpositive, Qpositive_plus w w'' = Qpositive_plus w' w'' -> w = w'.
proof: Proof. intros w w' w'' H. rewrite <- (Qpositive_sub_correct w' w''). rewrite <- (Qpositive_sub_correct w w''). rewrite H. auto. Qed.