proposition: Theorem add_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
proof: Proof. intros n m p q H1 H2. apply lt_trans with (m + p); [now apply add_lt_mono_r | now apply add_lt_mono_l]. Qed.
imports: NZAxioms NZBase NZMul NZOrder