Programmer avec Coq : récursion et filtrage dépendant