proposition: Corollary alpha_nat_odd n : (rem (alpha_nat (S n)) 2 = 1 \/ rem (alpha_nat n) 2 = 1)%nat.
proof: Proof. Proof using Hb_nat. destruct rem_2_is_0_or_1 with (x := alpha_nat (S n)) as [ H1 | ]; auto. destruct rem_2_is_0_or_1 with (x := alpha_nat n) as [ H2 | ]; auto. exfalso; generalize (alpha_nat_coprime n); intros (_ & _ & H3). destruct (H3 2%nat) as (? & ?); try lia; apply divides_rem_eq; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)