proposition: Fact divides_2_inv p : p div 2 -> p = 1 \/ p = 2.
proof: Proof. intros ([ | k ] & Hk); try discriminate. destruct p as [ | [ | [|] ] ]; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)