proposition: Lemma forNats_In : forall n i, i < n <-> In i (forNats n).
proof: Proof. induction n; intuition; simpl in *. lia. intuition. destruct (lt_dec i n). right. eapply IHn. trivial. left. lia. intuition; subst. lia. eapply Nat.lt_trans. eapply IHn. trivial. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation