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