proposition: Lemma allNatsLt_lt_if : forall (n i : nat), i < n -> In i (allNatsLt n).
proof: Proof. induction n; intuition; simpl in *. lia. eapply in_or_app. destruct (lt_dec i n). left. eauto. right. simpl. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation