proposition: Theorem le_lt_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 nlt_ge. now apply add_le_mono. Qed.
imports: NZAxioms NZBase NZMul NZOrder