proposition: Lemma Qplus_lt_le_compat : forall x y z t, x<y -> z<=t -> x+z < y+t.
proof: Proof. unfold Qplus, Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2); simpl; simpl_mult. Open Scope Z_scope. intros. match goal with |- ?a < ?b => ring_simplify a b end. rewrite Z.add_comm. apply Z.add_le_lt_mono. - match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. auto with zarith. - match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. do 2 (apply Z.mul_lt_mono_pos_r;try easy). Close Scope Z_scope. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool