proposition: Fact div_full q p : { n : nat & { r | q = n*p+r /\ (p <> 0 -> r < p) } }.
proof: Proof. case_eq p. + intro; exists 0, q; subst; split; auto; intros []; auto. + intros k H; destruct (@euclid q p) as (n & r & H1 & H2); try lia. exists n, r; rewrite <- H; split; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)