proposition: Fact euclid_2 n : exists q, n = 2*q \/ n = 1+2*q.
proof: Proof. exists (div n 2). generalize (div_rem_spec1 n 2) (@div_rem_spec2 n 2); intros; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)