proposition: Theorem Qpositive_sub_diff : forall w w' : Qpositive, w <> w' -> Qpositive_le w' w -> w <> Qpositive_sub w w'.
proof: Proof. intros w w' H H0. pattern w at 1 in |- *; rewrite <- (Qpositive_sub_correct w w'). red in |- *; intros H1. elim (Qpositive_plus_diff w w'). symmetry in |- *. apply Qpositive_sub_simpl_r with w'; auto. apply sym_not_equal; rewrite Qpositive_plus_sym; apply Qpositive_plus_diff. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. Qed.