proposition: Lemma div_ex : forall a b : nat, b <> 0 -> exists q : _, (exists r : _, is_div a b q r).
proof: Proof. intros a b H; apply diveucl_divex. apply eucl_dev. generalize H; case b; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)