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