proposition: Theorem iter_progression_app: forall a b n m, le m n -> b = next_n a m -> iter (progression a n) = g (iter (progression a m)) (iter (progression b (n - m))).
proof: Proof. intros a b n m H H0; unfold iter_progression; rewrite (progression_app a b n m); (try apply iter_app); auto. Qed.
imports: List Permutation Arith