proposition: Theorem Qpositive_sub_sub_assoc_l : forall w w' w'' : Qpositive, w <> Qpositive_plus w' w'' -> Qpositive_le (Qpositive_plus w' w'') w -> Qpositive_sub (Qpositive_sub w w') w'' = Qpositive_sub w (Qpositive_plus w' w'').
proof: Proof. intros w w' w'' Hnot Hle. cut (w <> w'). cut (Qpositive_le w' w). cut (w <> w''). cut (Qpositive_le w'' w). intros Hnot1 Hle1 Hnot2 Hle2. apply Qpositive_plus_simpl with w''. rewrite Qpositive_sub_correct2; auto with *. apply Qpositive_plus_simpl with w'. rewrite Qpositive_sub_correct2; auto with *. rewrite Qpositive_plus_assoc. rewrite (Qpositive_plus_sym w''). rewrite Qpositive_sub_correct2; auto with *. red in |- *; intros H; elim Hnot. rewrite <- H. rewrite Qpositive_plus_sym; rewrite Qpositive_sub_correct2; auto. rewrite <- (Qpositive_sub_correct w'' w'). apply Qpositive_le_sub_r; auto. apply sym_not_equal; rewrite Qpositive_plus_sym; apply Qpositive_plus_diff. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. rewrite Qpositive_plus_sym; auto. apply Qpositive_le_trans with (Qpositive_plus w' w''). rewrite Qpositive_plus_sym; apply Qpositive_plus_le. auto. red in |- *; intros H. elim Hnot. apply Qpositive_le_antisym. rewrite H; rewrite Qpositive_plus_sym; apply Qpositive_plus_le. exact Hle. apply Qpositive_le_trans with (Qpositive_plus w' w''); auto. apply Qpositive_plus_le. red in |- *; intros H. elim Hnot. apply Qpositive_le_antisym. rewrite H; apply Qpositive_plus_le. apply Hle. Qed.