proposition: Theorem progression_app: forall a b n m, le m n -> b = next_n a m -> progression a n = app (progression a m) (progression b (n - m)).
proof: Proof. intros a b n m; generalize a b n; clear a b n; elim m; clear m; simpl. intros a b n H H0; apply f_equal2 with ( f := progression ); auto with arith. intros m H a b n; case n; simpl; clear n. intros H1; absurd (0 < 1 + m); auto with arith. intros n H0 H1; apply f_equal2 with ( f := @cons A ); auto with arith. Qed.
imports: List Permutation Arith