proposition: Lemma allNatsLt_NoDup : forall (n : nat), NoDup (allNatsLt n).
proof: Proof. induction n; simpl in *; intuition. econstructor. eapply app_NoDup; intuition. econstructor. simpl; intuition. econstructor. simpl in *. intuition; subst. eapply allNatsLt_lt in H. lia. simpl in *. intuition; subst. eapply allNatsLt_lt in H0. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation