proposition: Lemma kseq_prop : forall (k : nat -> nat) (n : nat), (forall i : nat, 1 <= k i /\ k i <= n) -> (forall i : nat, k (S i) <= k i) -> {j : nat | S j < 2 * n /\ k j = k (S j) /\ k (S j) = k (S (S j))}.
proof: Proof. intros k n. generalize k; clear k. induction n as [| n Hrecn]; intros k H H0. elim (H 0); intros H1 H2. generalize (Nat.le_trans _ _ _ H1 H2); intro H3. exfalso. inversion H3. elim (eq_nat_dec (k 0) (k 2)). intro H1. exists 0. cut (k 0 = k 1). intro H2. repeat split. lia. assumption. rewrite <- H1. auto. apply Nat.le_antisymm. rewrite H1. apply H0. apply H0. intro H1. elim (Hrecn (fun m : nat => k (S (S m)))). 3: intro; apply H0. intros m Hm. exists (S (S m)); lia. intro i. split. elim (H (S (S i))); auto. elim (lt_eq_lt_dec (k 0) (k 2)); intro H2. elim H2; intro H3. generalize (H0 0); intro H4. generalize (H0 1); intro H5. lia. tauto. generalize (H 0); intro H3. elim H3; intros H4 H5. generalize (Nat.lt_le_trans _ _ _ H2 H5); intro H6. cut (k 2 <= n). 2: lia. intro H7. induction i as [| i Hreci]. assumption. apply Nat.le_trans with (k (S (S i))); auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)