proposition: Lemma allNatsLt_length : forall n, length (allNatsLt n) = n.
proof: Proof. induction n; intuition; simpl in *. rewrite app_length. rewrite IHn. rewrite Nat.add_comm. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation