proposition: Lemma Zlt_plus_plus : forall m n p q : Z, (m < n)%Z -> (p < q)%Z -> (m + p < n + q)%Z.
proof: Proof. intros. apply Z.lt_trans with (m := (n + p)%Z). rewrite Zplus_comm. rewrite Zplus_comm with (n := n). apply Zplus_lt_compat_l. assumption. apply Zplus_lt_compat_l. assumption. Qed.
imports: Coq(Lia)