proposition: Lemma nth_allNatsLt : forall k n, nth n (allNatsLt k) n = n.
proof: Proof. intuition. destruct (lt_dec n k). eapply nth_allNatsLt_lt; intuition. eapply nth_overflow. rewrite allNatsLt_length. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation