# Z_3: left inversion lemma. How to add 1 + 1 + 1

I am stuck. I want to prove left inversion lemma for Z_3

``````(* aux lemma)
Lemma Z_3_inv_lemma (k: nat) : ((3 + k) <? 3 = true) -> False.
Proof.
intro. induction k as [| k' IH].
- simpl in H. inversion H.
- rewrite Nat.add_succ_r in H. auto.
Qed.

(* main theorem *)
Proposition Z3_left_inv : forall x: Z_3, Z3_op (Z_3_inv x) x = z3_0.
Proof.
intro. unfold Z3_op. destruct x as [vx prf]. unfold z3_0. apply Z3_eq. destruct vx as [| vx'].
- simpl. reflexivity.
- destruct vx'.
+ simpl. reflexivity.
+ destruct vx'.
* simpl. reflexivity.
* revert prf. rewrite <- Nat.add_1_l. rewrite <- (Nat.add_1_l (S vx')). rewrite <- (Nat.add_1_l vx'). repeat rewrite Nat.add_assoc. change (1+1+1) with 3. intro.
``````

Result:

``````1 subgoal (ID 153)

vx' : nat
prf : (3 + vx' <? 3) = true
============================
(Z_3_inv {| n := 3 + vx'; proof := prf |} +
{| n := 3 + vx'; proof := prf |}) mod 3 = 0
``````

I want finish the proof by using Z_3_inv_lemma to prf and get False in the context. But when I do `apply Z_3_inv_lemma in prf.`, it gives an error:

``````Error: Cannot change prf, it is used in conclusion.
``````