proposition: Theorem map_nth_in : forall (A B : Set)(ls : list A)(f : A -> B) i defa defb, i < length ls -> nth i (map f ls) defb = f (nth i ls defa).
proof: Proof. induction ls; destruct i; intuition; simpl in *. lia. lia. eapply IHls. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation