proposition: Theorem add_le_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 n p) as [H1 | H1]. - now left. - destruct (le_gt_cases m q) as [H2 | H2]. + now right. + contradict H; rewrite nle_gt. now apply add_lt_mono. Qed.
imports: NZAxioms NZBase NZMul NZOrder