proposition: Theorem Qpositive_sub_simpl_r : forall w w' w'' : Qpositive, w <> w'' :>Qpositive -> w' <> w'' :>Qpositive -> Qpositive_le w'' w -> Qpositive_le w'' w' -> Qpositive_sub w w'' = Qpositive_sub w' w'' -> w = w'.
proof: Proof. intros w w' w'' H H0 H1 H2 H3. rewrite <- (Qpositive_sub_correct2 w w''); auto with *. rewrite <- (Qpositive_sub_correct2 w' w''); auto with *. rewrite H3; auto. Qed.