proposition: Theorem firstn_allNatsLt_h : forall ls n1 n2, n2 >= n1 -> ls = (allNatsLt n2) -> firstn n1 ls = allNatsLt n1.
proof: Proof. induction ls using rev_ind; intuition; simpl in *. symmetry in H0. eapply allNatsLt_nil_inv in H0. subst. assert (n1 = O). lia. subst. simpl. trivial. destruct n2; simpl in *. eapply app_eq_nil in H0. intuition. discriminate. eapply app_inj_tail in H0. intuition. subst. destruct (le_gt_dec n1 (length (allNatsLt n2))). rewrite firstn_app. eapply (@IHls); eauto. rewrite allNatsLt_length. trivial. trivial. rewrite allNatsLt_length in g. assert (n1 = (S n2)). lia. subst. eapply firstn_ge_all. rewrite allNatsLt_length. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation