proposition: Fact division_by_even n d : d <> 0 -> { q : nat & { j | arem n d q j } }.
proof: Proof. intros Hd. destruct (@euclid n (2*d)) as (q & r & H1 & H2); try lia. destruct (le_lt_dec r d) as [ Hr | Hr ]. + exists q, r; split; auto; left. rewrite H1; ring. + exists (S q), (2*d-r); split; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)