Z_3: left inversion lemma

Question

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.

Answer 1

I believe you can try pose proof (Z_3_inv_lemma vx' prf), that should get you an usable False.