proposition: Lemma firstn_ge_all : forall n (A : Set) (ls : list A), n >= length ls -> firstn n ls = ls.
proof: Proof. induction n; intuition idtac; simpl in *. destruct ls; simpl in *. trivial. lia. destruct ls. trivial. f_equal. eapply IHn. simpl in *. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation