proposition: Theorem mdiv_div : forall (d : nat) (a b : mon d), mdiv d b a -> mult_mon d (div_mon d a b) b = a.
proof: Proof. intros d a b H'; elim H'; simpl in |- *; auto. intros d0 v v' n n' H'0 H'1 H'2. rewrite Nat.sub_add; auto. rewrite H'2; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)