proposition: Lemma mult_sym : forall a b : nat, a * b = b * a.
proof: Proof. intros a b; elim a; simpl in |- *; auto with arith. intros y H. replace (y * b) with (b * y). elim (mult_n_Sm b y). apply plus_comm. Qed.
imports: Plus Mult Minus Lt Le Gt