coq - prove a lemma sum of all elements of a list l is equal to n, (sortascend n) is equal to n

Question

following is the one I'm having trouble with.

Lemma  sum_asc_dec_eq : forall k1 n , 
 addmem_list( k1) = n -> 
 addmem_list( sort_des k1) = n 
->  addmem_list( sort_asc k1)=n .
 Proof.
intros . induction k1 . 
+ simpl; auto. 
+ simpl in *.   induction n .
-  simpl.      

Abort.

question from:https://stackoverflow.com/questions/65617523/prove-a-lemma-sum-of-all-elements-of-a-list-l-is-equal-to-n-sortascend-n-is-e

Answer 1

Waitting for answers