proposition: Lemma allNatsLt_lt : forall n v, In v (allNatsLt n) -> v < n.
proof: Proof. induction n; intuition; simpl in *. lia. apply in_app_or in H. simpl in *. intuition; subst. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation