proposition: Lemma chain_build n : inhabited (chain n).
proof: Proof. Proof using HA1 HA2. induction n as [|n [c]]. - apply inhabits. split with (fun _ => rho 0). + easy. + intros m H. exfalso; lia. - cbn -[N P Pr] in HA2. destruct (@HA2 (c n)) as [pl [d [pr [[H1 H2] H3]]]]. 1: { rewrite ! iN_spec. 2:cbn; reflexivity. apply chain_N. easy. } rewrite !iP_spec in H1,H2. 1:rewrite !iPr_spec in H3. 2-9: cbn; easy. apply inhabits. pose (fun m => if m =? S n then d else c m) as f. split with f. + unfold f. destruct (Nat.eqb_neq 0 (S n)) as [_ ->]. 2:lia. apply chain_zero. + unfold f. destruct (Nat.eqb_neq 0 (S n)) as [_ ->]. 2:lia. intros m Hm. destruct (Nat.eqb_neq m (S n)) as [_ ->]. 2:lia. destruct (S m=?S n) eqn:Heq. * apply Nat.eqb_eq in Heq. assert (m=n) as -> by lia. exists pr, pl. rewrite chain_zero. split. 1:split. all:easy. * apply chain_succ. apply Nat.eqb_neq in Heq. lia. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions