proposition: Theorem firstn_allNatsLt : forall n1 n2, n2 >= n1 -> firstn n1 (allNatsLt n2) = allNatsLt n1.
proof: Proof. intuition. eapply firstn_allNatsLt_h; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation