proposition: Theorem le_sub_l : forall n m, n - m <= n.
proof: Proof. intros n m; induct m. - rewrite sub_0_r; now apply eq_le_incl. - intros m IH. rewrite sub_succ_r. apply le_trans with (n - m); [apply le_pred_l | assumption]. Qed.
imports: NMulOrder