proposition: Theorem succ_add_discr : forall n m, m ~= S (n + m).
proof: Proof. intros n m; induct m. - apply neq_sym. apply neq_succ_0. - intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. unfold not in IH; now apply IH. Qed.
imports: NBase