proposition: Lemma chain_lower (l:nat) (h:nat) (c:chain h): l > 0 -> l <= h -> {cc : chain l & forall k, k <= l -> chainData c k = chainData cc k}.
proof: Proof. intros Hl Hh. revert c. assert (h=(h-l)+l) as -> by lia. generalize (h-l). intros dh c. induction dh as [|dh IH]. - now exists c. - destruct (chain_inversion c) as [[[[n pl] ph] cc] ->]. fold Nat.add in cc. destruct (IH cc) as [cc' Hcc']. exists cc'. intros k Hk. cbn [chainData]. destruct (Dec (S dh + l = k)) as [Hf|_]. + lia. + apply Hcc'. lia. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)