proposition: Theorem CRT_bin_informative : { w | rem w u = rem a u /\ rem w v = rem b v /\ 2 < w }.
proof: Proof. Proof using Hu Hv Huv. destruct bezout_rel_prime with (1 := Huv) as (x & y & H1). assert (rem (x*u) v = rem 1 v) as H2. { rewrite rem_plus_div with (a := 1) (b := u*v); auto. rewrite <- H1; apply rem_plus_div; auto. } assert (rem (y*v) u = rem 1 u) as H3. { rewrite rem_plus_div with (a := 1) (b := u*v); auto. rewrite <- H1, Nat.add_comm. apply rem_plus_div; auto. } exists (3*(u*v)+a*(y*v)+b*(x*u)); msplit 2. + rewrite <- rem_plus_rem, (Nat.mul_assoc b). rewrite rem_scal with (k := b*x), rem_diag; auto. rewrite Nat.mul_0_r, rem_of_0, Nat.add_0_r. rewrite <- rem_plus_rem, rem_scal, H3, <- rem_scal, Nat.mul_1_r. rewrite rem_plus_rem, Nat.add_comm. symmetry; apply rem_plus_div; auto. + rewrite <- Nat.add_assoc, (Nat.add_comm (a*_)), Nat.add_assoc. rewrite <- rem_plus_rem, (Nat.mul_assoc a). rewrite rem_scal with (k := a*y), rem_diag; auto. rewrite Nat.mul_0_r, rem_of_0, Nat.add_0_r. rewrite <- rem_plus_rem, rem_scal, H2, <- rem_scal, Nat.mul_1_r. rewrite rem_plus_rem, Nat.add_comm. symmetry; apply rem_plus_div; auto. + apply Nat.lt_le_trans with (3*1); try lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd prime binomial) Undecidability.Shared.Libs.DLW.Vec(pos vec)