proposition: Lemma nth_allNatsLt_lt : forall k n, n < k -> nth n (allNatsLt k) n = n.
proof: Proof. induction k; intuition; simpl in *. lia. destruct (lt_dec n k). rewrite app_nth1. eauto. rewrite allNatsLt_length. trivial. rewrite app_nth2. rewrite allNatsLt_length. assert (k = n). lia. rewrite H0. rewrite Nat.sub_diag. simpl. trivial. rewrite allNatsLt_length. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation