proposition: Lemma chain_exists_lower (l h :nat) (cl:chain l) (ch:chain h) : l<=h -> (forall k, k <= l -> chainData cl k = chainData ch k) -> incl (chain_exists cl) (chain_exists ch).
proof: Proof. intros Hlh. revert ch. assert (h=(h-l)+l) as -> by lia. generalize (h-l) as dh. intros dh ch Heq. induction dh as [|dh IHdh]. - now rewrite (@chain_data_unique l cl ch). - destruct (chain_inversion ch) as [[[[n pl] ph] ch'] Hch]; fold Nat.add in *. rewrite Hch. cbn; do 8 apply incl_tl. apply (IHdh ch'). intros k Hk. rewrite Hch in Heq. specialize (Heq k Hk). cbn [chainData] in Heq. destruct (Dec (S dh + l =k)) as [Ht|Hf]; [lia|easy]. 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)