proposition: Lemma mult_permute : forall a b c : nat, a * b * c = a * c * b.
proof: Proof. intros. rewrite mult_assoc_reverse. rewrite mult_assoc_reverse. replace (c * b) with (b * c); auto with arith. Qed.
imports: Plus Mult Minus Lt Le Gt