# Software Foundations/ Verified Functional Algorithms Ejercicio

**URL:** <https://discourse.rocq-prover.org/t/software-foundations-verified-functional-algorithms-ejercicio/1056>\
**Category:** \[es\] ¡Rocq en español!\
**Created:** [September 17, 2020, 7:06pm UTC](https://discourse.rocq-prover.org/t/software-foundations-verified-functional-algorithms-ejercicio/1056 "2020-09-17T19:06:22Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Cristina](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cristina/32/302_2.png) [@Cristina](https://discourse.rocq-prover.org/u/Cristina)\
**Post date:** [September 17, 2020, 7:06pm UTC](https://discourse.rocq-prover.org/t/software-foundations-verified-functional-algorithms-ejercicio/1056/1 "2020-09-17T19:06:22Z")

</div>

Hola buenas, he estado intentando resolver los ejercicios de la parte de merge del libro Verified Functional Algorithms y estoy teniendo un problema con uno.  
Lemma sorted\_merge : forall l1, sorted l1 -\>  
forall l2, sorted l2 -\>  
sorted (merge l1 l2).  
Proof.

intros. induction l1.

- simpl. induction l2.
  - auto.
  - auto.

- induction l2.
  - auto.
  - simpl. bdestruct (a\<=?a0).
    - inv H.  
\*\* auto. constructor. auto. auto.  
\*\* apply sorted\_merge1. auto. auto. auto.
    - 

Esto es lo que he conseguido hacer. Supongo que ahora tendré que hacer otra inducción en l2 pero haciendo eso solo me complico más.

Muchas gracias