proposition: Theorem le_le_add_le : forall n m p q, n <= m -> p + m <= q + n -> p <= q.
proof: Proof. intros n m p q H1 H2. destruct (le_gt_cases p q); [assumption |]. contradict H2. rewrite nle_gt. now apply add_lt_le_mono. Qed.
imports: NZAxioms NZBase NZMul NZOrder