proposition: Lemma Qplus_lt_compat : forall x y z t : Q, x < y -> z < t -> x + z < y + t.
proof: Proof. intros x y z t H1 H2. apply Qplus_lt_le_compat. - assumption. - apply Qle_lteq; left; assumption. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool