proposition: Theorem allNatsLt_nil_inv : forall n, allNatsLt n = nil -> n = O.
proof: Proof. destruct n; intuition; simpl in *. eapply app_eq_nil in H. intuition. discriminate. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation