proposition: Theorem Zprogression_opp: forall n m, rev (progression Z.succ n m) = progression Z.pred (n + Z_of_nat (pred m)) m.
proof: Proof. intros n m; generalize n; elim m; clear n m. simpl; auto. intros m Hm n. rewrite (Zprogression_end n); auto. rewrite distr_rev. rewrite Hm; simpl; auto. case m. simpl; auto. intros m1; replace (n + Z_of_nat (pred (S m1))) with (Z.pred (n + Z_of_nat (S m1))); auto. rewrite inj_S; simpl; (unfold Z.pred; unfold Z.succ); auto with zarith. Qed.
imports: Iterator ZArith Lia UList