proposition: Theorem Qpositive_plus_sub_assoc : forall w w' w'' : Qpositive, w <> w' -> Qpositive_le w' w -> Qpositive_plus (Qpositive_sub w w') w'' = Qpositive_sub (Qpositive_plus w w'') w'.
proof: Proof. intros w w' w'' H H0. apply Qpositive_plus_simpl with w'. rewrite Qpositive_plus_assoc. rewrite (Qpositive_plus_sym w''). rewrite <- Qpositive_plus_assoc. rewrite Qpositive_sub_correct2; auto with *. rewrite Qpositive_sub_correct2; auto with *. red in |- *; intros H1; elim (Qpositive_plus_diff w w''). apply Qpositive_le_antisym. apply Qpositive_plus_le. rewrite H1; exact H0. apply Qpositive_le_trans with w; auto. apply Qpositive_plus_le. Qed.