The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-06T15:23:12+05:30, soham chakraborty wrote:

> On the solution you sent Coq is getting stuck at
>
> Case "n = O". Error: No interpretation for string "n = O".
>
> Can you please check.

As Valentin said, you have to load some code from the book to use the
Case notation.  Otherwise you can just comment out the Case sentences,
and the proof will work without any other code:

Theorem mult_1_l :
  forall n : nat,
    1 * n = n.

Proof.
  intros n.
  induction n as [ | p IHp].
  {
    (* Case "n = O". *)
    reflexivity.
  }
  {
    (* Case "n = S p". *)
    simpl.
    simpl in IHp.
    rewrite -> IHp.
    reflexivity.
  }
Qed.

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/