theorem symmetricZPlus: symmetric Z Zplus.
change with (\forall a,b:Z. (Zplus a b) = (Zplus b a)).
theorem symmetricZPlus: symmetric Z Zplus.
change with (\forall a,b:Z. (Zplus a b) = (Zplus b a)).
lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
intros.
lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
intros.