proposition: Theorem mult_div_id : forall (d : nat) (a : mon d), div_mon d a a = zero_mon d.
proof: Proof. intros d a; elim a; simpl in |- *; auto. intros d0 n m H'; rewrite H'; auto. rewrite Nat.sub_diag; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)