proposition: Lemma In_iota (n m k : nat) : (n <= m <= k)%nat <-> In m (iota n (S k - n)).
proof: Proof. generalize (mem_iota n (S k - n) m). case: In_mem => // H H0. apply sym_eq in H0. case/andP: H0 => H0 H1. apply Rcomplements.SSR_leq in H0. apply SSR_leq in H1. change ssrnat.addn with Peano.plus in H1. split => // _. split => //. case: (le_dec n (S m)). intro ; lia. intro H2. rewrite (proj2 (Nat.sub_0_le _ _)) in H1 => //. contradict H2. by eapply Nat.le_trans, Nat.le_succ_diag_r. contradict H2. by eapply Nat.le_trans, Nat.le_succ_diag_r. change ssrnat.addn with Peano.plus in H0. split => // H1. case: H1 => /= H1 H2. apply sym_eq in H0. apply Bool.andb_false_iff in H0. case: H0 => //. move/SSR_leq: H1 ; by case: ssrnat.leq. rewrite Nat.add_comm Nat.sub_add; [| lia]. move/le_n_S/SSR_leq: H2 ; by case: ssrnat.leq. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements