proposition: Lemma forNats_NoDup : forall n, NoDup (forNats n).
proof: Proof. induction n; intuition; simpl in *; econstructor; intuition. assert (n < n). eapply forNats_In. trivial. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation