proposition: Fact nat2Zp_minus u v : v <= u -> 〚u-v〛=〚u〛⊕ ∸〚v〛.
proof: Proof. intros; apply Zp_inj; simpl. rewrite rem_plus_rem, (Nat.add_comm (rem _ _)), Nat.add_comm. generalize (div u p) (div v p) (div_rem_spec1 u p) (div_rem_spec1 v p). intros a b H1 H2. assert (b <= a) as Hab. { destruct (le_lt_dec b a); auto. replace b with ((1+a) + (b-a-1)) in H2 by lia. generalize (div_rem_spec2 u Hp) (div_rem_spec2 v Hp); intros H3 H4. do 2 rewrite Nat.mul_add_distr_r in H2. contradict H; rewrite H1, H2, Nat.mul_1_l. generalize (a* p) ((b-a-1)* p); intros; lia. } destruct (eq_nat_dec a b) as [ | Ha ]; try subst b. + assert (rem v p <= rem u p) as H3. { rewrite H1, H2 in H; revert H; intros; lia. } symmetry; apply rem_erase with 1. rewrite H1 at 2. rewrite H2 at 2. generalize (a* p) (div_rem_spec2 v Hp); intros; lia. + apply rem_erase with (a-b-1). rewrite H2 at 1; rewrite H1 at 1. do 2 rewrite Nat.mul_sub_distr_r. rewrite Nat.mul_1_l. assert (b* p + p <= a* p) as E. { replace a with (1+b+(a-b-1)) by lia. do 2 rewrite Nat.mul_add_distr_r. generalize (b* p) ((a-b-1)* p); intros; lia. } revert E. generalize (a* p) (b* p) (div_rem_spec2 u Hp) (div_rem_spec2 v Hp); intros. lia. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)