proposition: Theorem Qpositive_sub_simpl_l : 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. apply Qpositive_plus_simpl with (Qpositive_sub w'' w). rewrite (Qpositive_plus_sym w). rewrite Qpositive_sub_correct2; auto. rewrite (Qpositive_plus_sym w'). rewrite H3. rewrite Qpositive_sub_correct2; auto with *. Qed.