proposition: Lemma diveucl_divex : forall a b : nat, diveucl a b -> exists q : _, (exists r : _, is_div a b q r).
proof: Proof. intros a b H; case H. intros q r H' H'0; exists q; exists r; split; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)