proposition: Theorem Qplus_lt_compat_r : ∀ x y z, x < y → x + z < y + z.
proof: Proof. intros (x₁, x₂) (y₁, y₂) (z₁, z₂) H. unfold Qlt in H; simpl in H. unfold Qlt, Qplus; simpl. do 2 rewrite Pos2Z.inj_mul. do 2 rewrite Z.mul_add_distr_r. do 4 rewrite Z.mul_assoc. remember (z₁ * Zpos y₂ * Zpos x₂ * Zpos z₂)%Z as t. remember (z₁ * Zpos y₂ * Zpos x₂)%Z as u. rewrite Z.mul_shuffle0 in Hequ. subst u. rewrite <- Heqt. apply Zplus_lt_compat_r. clear t Heqt. rewrite <- Zmult_assoc. rewrite Z.mul_shuffle1. remember (y₁ * Zpos z₂ * Zpos x₂ * Zpos z₂)%Z as t. rewrite <- Zmult_assoc in Heqt. rewrite Z.mul_shuffle1 in Heqt; subst t. apply Zmult_lt_compat_r; [ idtac | assumption ]. rewrite <- Pos2Z.inj_mul. apply Pos2Z.is_pos. Qed.
imports: Utf8 QArith NPeano Sorted Psatz