proposition: Theorem add_lt_cases : forall n m p q, n + m < p + q -> n < p \/ m < q.
proof: Proof. intros n m p q H; destruct (le_gt_cases p n) as [H1 | H1]; [| now left]. destruct (le_gt_cases q m) as [H2 | H2]; [| now right]. contradict H; rewrite nlt_ge. now apply add_le_mono. Qed.
imports: NZAxioms NZBase NZMul NZOrder