proposition: Theorem Qpositive_sub_le : forall w w' : Qpositive, w <> w' -> Qpositive_le w' w -> Qpositive_le (Qpositive_sub w w') w.
proof: Proof. intros w w' H H1; pattern w at 2 in |- *; 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. apply Qpositive_plus_le. Qed.