proposition: Theorem lt_le_add_lt : 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 q p); [| assumption]. contradict H2. rewrite nle_gt. now apply add_le_lt_mono. Qed.
imports: NZAxioms NZBase NZMul NZOrder