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