proposition: Lemma chain_proves_rel (h:nat) (c:chain h) (i:nat) : i <= h -> In (Pr $(findPairLow c i) $(findPairHigh c i)) (chain_exists c).
proof: Proof. intros H. induction c as [|h n pl pr cc IH]. - now left. - destruct (Dec ((S h) = i)) eqn:Heq. + do 7 right. left. unfold findPairLow,findPairHigh,chainData. now rewrite Heq. + do 8 right. unfold findPairLow, findPairHigh, chainData. rewrite Heq. apply IH. 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)