Injectivity of quotient constructor would lead to proof of false

quot.lean

def zmod : Nat -> Type | n => Quot (fun a b => a % n = b % n)

theorem prop_true_or_false : (p:Prop) -> p = False ∨ p = True := by
  exact fun p => Or.symm (Classical.propComplete p)

theorem quot_ctor_inj : Quot.mk f a = Quot.mk f b -> a = b := by 
  intro k
  -- injection k
  admit 


def Quot.project : @Quot T f -> T := by
  intro k 
  refine Quot.lift id ?_ k
  simp
  intro a b
  let k := prop_true_or_false (f a b)
  match k with 
  | .inl c => 
    rw [c]
    apply False.elim
  | .inr _ =>
    intro i
    let p := Quot.sound (r:=f) (a:=a) (b:=b) i
    exact quot_ctor_inj p


-- #check Quot.sound

def ex1 : zmod 3 := Quot.mk _ 2

def zmod_add : zmod 3 -> zmod 3 -> zmod 3 
| a, b => Quot.mk _ (((Quot.project a) + (Quot.project b)) % 3)

#reduce zmod_add ex1 ex1


example : zmod_add ex1 ex1 = Quot.mk _ 1 := rfl


example : Quot.mk (fun _ _ => True) 1 = Quot.mk (fun _ _ => True) 2 -> False := by
  intro p
  let _ := quot_ctor_inj p
  contradiction