proposition: Lemma plus_permute2 : forall x y z : nat, x + y + z = x + z + y.
proof: Proof. intros. rewrite (plus_comm x y). rewrite (plus_comm x z). rewrite plus_comm. symmetry in |- *. rewrite plus_comm. rewrite plus_permute. auto with arith. Qed.
imports: Plus Mult Minus Lt Le Gt