proposition: Lemma injection_spec k1 k2 n m : k1 < 4 -> k2 < 4 -> inj k1 n = inj k2 m -> k1 = k2 /\ n = m.
proof: Proof. intros. unfold inj in *. lia. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10.ArithLibs(Zp lagrange) Undecidability.H10.Dio(dio_logic dio_single) Undecidability.H10(H10 H10_undec) Undecidability.H10(H10Z) Undecidability.H10.ArithLibs(Zp lagrange) Undecidability.Synthetic.Definitions