proposition: Theorem Qpositive_le_sub_simpl_l : forall x y z : Qpositive, Qpositive_le x z -> Qpositive_le y z -> z <> x -> z <> y -> Qpositive_le (Qpositive_sub z x) (Qpositive_sub z y) -> Qpositive_le y x.
proof: Proof. intros x y z H H0 H1 H2 H3. replace y with (Qpositive_sub z (Qpositive_sub z y)). replace x with (Qpositive_sub z (Qpositive_sub z x)). apply Qpositive_le_sub_l. apply sym_not_equal; apply Qpositive_sub_diff; auto. apply sym_not_equal; apply Qpositive_sub_diff; auto. apply Qpositive_sub_le; auto. apply Qpositive_sub_le; auto. auto. rewrite Qpositive_sub_sub_assoc; auto. rewrite Qpositive_plus_sym; rewrite Qpositive_sub_correct; auto. apply Qpositive_sub_diff. auto. auto. apply Qpositive_sub_le; auto. rewrite Qpositive_sub_sub_assoc; auto. rewrite Qpositive_plus_sym; rewrite Qpositive_sub_correct; auto. apply Qpositive_sub_diff. auto. auto. apply Qpositive_sub_le; auto. Qed.