proposition: Theorem sub_add_le : forall n m, n <= n - m + m.
proof: Proof. intros n m. destruct (le_ge_cases n m) as [LE|GE]. - rewrite <- sub_0_le in LE. rewrite LE; nzsimpl. now rewrite <- sub_0_le. - rewrite sub_add by assumption. apply le_refl. Qed.
imports: NMulOrder