proposition: Lemma mult_div_q : forall x y q r : nat, is_div (x * y) y q r -> q = x.
proof: Proof. intros x y q r (H1, H2). apply div_unic_q with (a := x * y) (b := y) (r1 := r) (r2 := 0); split; auto. apply Nat.le_lt_trans with (m := r); auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)