proposition: Theorem mult_mon_assoc : forall (d : nat) (a b c : mon d), mult_mon d a (mult_mon d b c) = mult_mon d (mult_mon d a b) c.
proof: Proof. intros d; elim d; simpl in |- *; auto. intros n H' a b c. rewrite (H' (pmon2 (S n) a) (pmon2 (S n) b) (pmon2 (S n) c)); auto. rewrite (Nat.add_assoc (pmon1 (S n) a) (pmon1 (S n) b) (pmon1 (S n) c)); auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)