proposition: Lemma add_comm3 : forall x y z, x + (y + z) = (z + y) + x.
proof: Proof. intros x y z. rewrite add_comm. rewrite add_comm. Abort. Lemma add_comm3_take3 : forall x y z, x + (y + z) = (z + y) + x. Proof. intros x y z. rewrite add_comm. rewrite (add_comm y z). reflexivity. Qed.