proposition: Lemma Zle_lt_plus_plus : forall m n p q : Z, (m <= n)%Z -> (p < q)%Z -> (m + p < n + q)%Z.
proof: Proof. intros. case (Zle_lt_or_eq m n). assumption. intro. apply Zlt_plus_plus. assumption. assumption. intro. rewrite H1. apply Zplus_lt_compat_l. assumption. Qed.
imports: Coq(Lia)