proposition: Theorem Qpositive_sub_sub_assoc : forall w w' w'' : Qpositive, w' <> w'' -> Qpositive_le w'' w' -> w <> Qpositive_sub w' w'' -> Qpositive_le (Qpositive_sub w' w'') w -> Qpositive_sub w (Qpositive_sub w' w'') = Qpositive_sub (Qpositive_plus w w'') w'.
proof: Proof. intros w w' w'' H H0 H1 H2. apply Qpositive_plus_simpl with w'. rewrite Qpositive_sub_correct2; auto. apply Qpositive_plus_simpl with (Qpositive_sub w' w''). rewrite <- (Qpositive_plus_sym w'). rewrite Qpositive_plus_assoc. rewrite Qpositive_sub_correct2; auto. rewrite Qpositive_plus_assoc. rewrite (Qpositive_plus_sym w''). rewrite Qpositive_sub_correct2; auto. apply Qpositive_plus_sym. red in |- *; intros H3; try exact H3. elim H1; try assumption. rewrite <- H3; rewrite Qpositive_sub_correct; auto. rewrite <- (Qpositive_sub_correct2 w' w''); auto with *. apply Qpositive_le_add. auto. Qed.