proposition: Theorem binary_le_binomial n m : n ≲ m <-> rem (binomial m n) 2 = 1.
proof: Proof. split. + induction 1 as [ n | n m H1 H2 IH2 ]. * rewrite binomial_n0, rem_lt; lia. * rewrite lucas_lemma with (1 := prime_2) (2 := div_rem_spec1 m 2) (4 := div_rem_spec1 n 2); try (apply div_rem_spec2; lia). rewrite Nat.mul_comm, <- rem_mult_rem, IH2, Nat.mul_1_r. revert H1. generalize (rem_2_is_0_or_1 m) (rem_2_is_0_or_1 n). intros [ G1 | G1 ] [ G2 | G2 ]; rewrite G1, G2; intros; try lia. ++ rewrite binomial_n0, rem_lt; lia. ++ rewrite binomial_n0, rem_lt; lia. ++ rewrite binomial_n1, rem_lt; lia. + induction on n m as IH with measure m. destruct (eq_nat_dec m 0) as [ Hm | Hm ]. * destruct n; try (intros; constructor; fail). subst; rewrite binomial_gt, rem_lt; lia. * generalize (div_rem_spec1 m 2) (div_rem_spec1 n 2); intros H1 H2. rewrite lucas_lemma with (1 := prime_2) (2 := H1) (4 := H2); auto; try (apply div_rem_spec2; lia). rewrite rem_2_mult; intros (H3 & H4). apply IH in H3; try lia. constructor 2; auto. revert H4. generalize (rem_2_is_0_or_1 m) (rem_2_is_0_or_1 n). intros [ G1 | G1 ] [ G2 | G2 ]; rewrite G1, G2; intros; try lia. rewrite binomial_gt, rem_lt in H4; lia. Qed.
imports: Arith Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums bool_nat rel_iter) Undecidability.H10.ArithLibs(luca) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_expo)