proposition: Lemma Qplus_lt_l (x y z: Q): x + z < y + z <-> x < y.
proof: Proof. split; intros. - rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z). do 2 rewrite Qplus_assoc. apply Qplus_lt_le_compat; auto with *. - apply Qplus_lt_le_compat; auto with *. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool