CoqEx13.v

(* Q13 *)
Inductive pos : Set :=
  | S0 : pos
  | S : pos -> pos.

Fixpoint plus(n m:pos) : pos := 
  match n with
    | S0 => S m
    | S n => S (plus n m)
  end.

Infix "+" := plus.

Theorem plus_assoc : forall n m p : pos, n + (m + p) = (n + m) + p.
Proof.
  intros.
  induction n.
  simpl. 
  reflexivity.
  simpl.
  f_equal.
  apply IHn. 
  Qed.