proposition: Fact rem_2_is_0_or_1 x : rem x 2 = 0 \/ rem x 2 = 1.
proof: Proof. generalize (rem x 2) (@div_rem_spec2 x 2); intros; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)