proposition: Lemma div_x_O_q : forall x q r : nat, is_div 0 x q r -> q = 0.
proof: Proof. intros x q r H'. rewrite (div_x_O_r x q r) in H'; auto; case H'; intros H1 H2. case (mult_eqO q x); auto. rewrite H2; auto with arith. intros H'1; Contradict H1; auto; rewrite H'1; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)