proposition: Lemma reformulate_step_prop_index {Q : nat -> Prop} : (forall (k : nat) (n : nat -> nat), (forall l : nat, l <= k -> Q (n l)) -> (forall l : nat, l < k -> n l < n (l + 1)) -> {n_kplus1 : nat | Q n_kplus1 /\ n k < n_kplus1}) -> (forall (k : nat) (n : nat -> nat), (forall l : nat, l <= k -> index_seq_prop_family Q l n) -> {n_kplus1 : nat | forall l : nat, l <= k + 1 -> index_seq_prop_family Q l (const_seq_from n_kplus1 (k + 1) n)}).
proof: Proof. intros Hstep k n H. assert (forall l : nat, l <= k -> Q (n l)) as H1. { intros l le_k. induction l. - apply (H 0 le_k). - assert (S l = l + 1) as Sl_eq_lplus1 by lia; rewrite Sl_eq_lplus1. apply (proj1 (H (S l) le_k)). } assert (forall l : nat, l < k -> n l < n (l + 1)) as H2. { intros l lt_k. apply (proj2 (H (S l) lt_k)). } destruct (Hstep k n H1 H2) as [n_kplus1 Hn_kplus1]. exists n_kplus1. intros l le_kplus1. induction l. - simpl; unfold const_seq_from. destruct (lt_dec 0 (k + 1)) as [O_lt_kplus1 | not_O_lt_kplus1]. + assert (0 <= k) as O_le_k by lia. exact (H1 0 O_le_k). + exact (proj1 Hn_kplus1). - simpl; unfold const_seq_from. destruct (lt_dec (l + 1) (k + 1)) as [lplus1_lt_kplus1 | not_lplus1_lt_kplus1]. + split. * assert (l + 1 <= k) as lplus1_le_k by lia. exact (H1 (l + 1) lplus1_le_k). * destruct (lt_dec l (k + 1)) as [l_lt_kplus1 | not_l_lt_kplus1]. -- assert (S l <= k) as Sl_le_k by lia. exact (proj2 (H (S l) Sl_le_k)). -- assert False by lia; contradiction. + split. * exact (proj1 Hn_kplus1). * destruct (lt_dec l (k + 1)) as [l_lt_kplus1 | not_l_lt_kplus1]. -- assert (l = k) as l_eq_k by lia. rewrite l_eq_k. exact (proj2 Hn_kplus1). -- assert False by lia; contradiction. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric