proposition: Theorem add_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
proof: Proof. intros n m p q H1 H2. apply le_trans with (m + p); [now apply add_le_mono_r | now apply add_le_mono_l]. Qed.
imports: NZAxioms NZBase NZMul NZOrder