proposition: Theorem Zprogression_pred_end: forall n m, progression Z.pred n (S m) = app (progression Z.pred n m) (cons (n - Z_of_nat m) nil).
proof: Proof. intros n m; generalize n; elim m; clear n m. simpl; intros; apply f_equal2 with ( f := @cons Z ); auto with zarith. intros m1 Hm1 n1. apply trans_equal with (cons n1 (progression Z.pred (Z.pred n1) (S m1))); auto. rewrite Hm1. replace (Z.pred n1 - Z_of_nat m1) with (n1 - Z_of_nat (S m1)). auto. replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1). auto with zarith. rewrite inj_S; auto with zarith. Qed.
imports: Iterator ZArith Lia UList