proposition: Theorem sub_succ : forall n m, S n - S m == n - m.
proof: Proof. intros n m; induct m. - rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. - intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. Qed.
imports: NMulOrder