proposition: Theorem alpha_nat_2lm b n m l j v : 2 <= b -> v = alpha_nat b (S (S m)) - alpha_nat b m -> arem n (S m) l j -> rem (alpha_nat b n) v = rem (alpha_nat b j) v \/ rem (alpha_nat b n + alpha_nat b j) v = 0.
proof: Proof. intros Hb Hv. assert (Hv' : Z.of_nat v = (alpha_Z b (S(2 + m)) - alpha_Z b (S m))%Z). { rewrite Hv. rewrite Nat2Z.inj_sub; auto. apply Nat.lt_le_incl, alpha_nat_smono; lia. } intros (Hk & [ Hl | (Hl1 & Hl2) ] ). + destruct alpha_nat_2lm_plus_j with (Hb_nat := Hb) (Hv := Hv') (l := l) (j := j) as [ H | H ]. - rewrite nat2Zp_inj in H; subst; auto. - right; rewrite <- rem_of_0 with v. rewrite <- nat2Zp_inj with (Hp := alpha_SSm_m_neq_0 Hb (S m) Hv'). rewrite nat2Zp_plus, Hl, H, Zp_add_comm, Zp_minus, nat2Zp_zero; auto. + destruct alpha_nat_2lm_minus_j with (Hb_nat := Hb) (Hv := Hv') (l := l) (j := j) as [ H | H ]; auto. - rewrite nat2Zp_inj in H; subst; auto. - right; rewrite <- rem_of_0 with v. rewrite <- nat2Zp_inj with (Hp := alpha_SSm_m_neq_0 Hb (S m) Hv'). rewrite nat2Zp_plus, Hl2, H, Zp_add_comm, Zp_minus, nat2Zp_zero; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)