proposition: Theorem Qplus_cmp_compat_r : ∀ x y z, (x ?= y) = (x + z ?= y + z).
proof: Proof. intros (x₁, x₂) (y₁, y₂) (z₁, z₂). unfold Qcompare; 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. rewrite <- Zplus_cmp_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_cmp_compat_r. rewrite <- Pos2Z.inj_mul. apply Pos2Z.is_pos. Qed.
imports: Utf8 QArith NPeano Sorted Psatz