proposition: Theorem eq_add_succ : forall n m, (exists p, n + m == S p) <-> (exists n', n == S n') \/ (exists m', m == S m').
proof: Proof. intros n m; cases n. - split; intro H. + destruct H as [p H]. rewrite add_0_l in H; right; now exists p. + destruct H as [[n' H] | [m' H]]. * symmetry in H; false_hyp H neq_succ_0. * exists m'; now rewrite add_0_l. - intro n; split; intro H. + left; now exists n. + exists (n + m); now rewrite add_succ_l. Qed.
imports: NBase