proposition: Lemma Zsum_swap: forall (n m : Z) (f : Z -> Z), Zsum n m f = Zsum m n f.
proof: Proof. intros n m f; revert n m. cut (forall n m, n < m -> Zsum n m f = Zsum m n f). { intros L n m. destruct (Ztrichotomy n m) as [ LT | [ -> | GT ] ]. - apply L, LT. - reflexivity. - symmetry; apply L, Z.gt_lt, GT. } intros n m n_lt_m; unfold Zsum. replace (m <=? n) with false by (symmetry; apply Z.leb_gt, n_lt_m). replace (n <=? m) with true by (symmetry; apply Z.leb_le, Z.lt_le_incl, n_lt_m). apply iter_permutation; auto with zarith. apply permutation_trans with (rev (progression Z.succ n (Z.abs_nat ((1 + m) - n)))). apply permutation_sym; apply permutation_rev. rewrite Zprogression_opp; auto with zarith. replace (n + Z_of_nat (pred (Z.abs_nat ((1 + m) - n)))) with m; auto. replace (Z.abs_nat ((1 + m) - n)) with (S (Z.abs_nat (m - n))). simpl. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. lia. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression