proposition: Lemma IB_F_succ_right rho : rho_canon rho -> rho ⊨ F_succ_right.
proof: Proof. intros H0. unfold F_succ_right. intros a' y' c b a y x Hr1 Hr2 Hr3 Hr4. eapply IB_erel_e in Hr1, Hr2, Hr3, Hr4. cbn in Hr1,Hr2,Hr3,Hr4. destruct Hr1 as (x_1&y_1&a_1&b_1&He11&He12&He13&He14&Hr1'). destruct Hr2 as (b_2&y_2&c_1&b_3&He21&He22&He23&He24&Hr2'). destruct Hr3 as (y_3&v0_1&y'_1&v0_2&He31&He32&He33&He34&Hr3'). destruct Hr4 as (a_2&v0_3&a'_1&v0_4&He41&He42&He43&He44&Hr4'). rewrite H0 in He32,He34,He42,He44. set_eq v0_1 0. set_eq v0_2 0. set_eq v0_3 0. set_eq v0_4 0. set_eq a_2 a_1. set_eq b_2 b_1. set_eq b_3 b_1. set_eq y_2 y_1. set_eq y_3 y_1. eapply IB_erel_i; cbn. 1-4:eauto. 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