Context: I'm working on exercises in Software Foundations.

Theorem neg_move : forall x y : bool,
  x = negb y -> negb x = y.
Proof. Admitted.

Theorem evenb_n__oddb_Sn : forall n : nat,
  evenb n = negb (evenb (S n)).
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".
    simpl. reflexivity.
  Case "n = S n'".
    rewrite -> neg_move.

Before the last line, my subgoal is this:

evenb (S n') = negb (evenb (S (S n')))

And I want to transform it into this:

negb (evenb (S n')) = evenb (S (S n'))

When I try to step through rewrite -> neg_move, however, it produces this error:

Error: Unable to find an instance for the variable y.

I'm sure this is really simple, but what am I doing wrong? (Please don't give anything away for solving evenb_n__oddb_Sn, unless I'm doing it completely wrong).

rocq-prover
Edit
Report