Functional Data Structures and Algorithms. A Proof Assistant Approach