proposition: Lemma IB_F_succ_left rho : rho_canon rho -> rho ⊨ F_succ_left.
proof: Proof. intros (H0&H1&H2). unfold F_succ_left. intros n Hc1. rewrite IB_Not. intros Hc. rewrite IB_wFalse; cbn; rewrite H1, H2; intros _. eapply (IB_N_e (n:=n) (i:=0) eq_refl Hc1). intros [m Hnm]. cbn in Hc. specialize (Hc (Pair m 0) (Num (S m)) (Pair (S m) 0)). eapply IB_P_e in Hc; cbn. 2-4: reflexivity. 2: eexists; eexists; repeat split; congruence. eapply IB_P_e in Hc; cbn. 2-4: reflexivity. 2: eexists; eexists; repeat split; congruence. cbn in Hc. rewrite IB_dFalse in Hc. 2-3: cbv; congruence. apply Hc. dn. lia. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Utils.FriedmanTranslationFragment 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) Coq(Arith Lia List) Undecidability.FOL.Reductions(H10UPC_to_FOL_constructions)