string - Coq 文字列ソート補題

Question

以下のように定義された文字列ソート関数があり、以下の補題を証明したいと思い sort_str_list_sameます。私は Coq の専門家ではありません。帰納法を使用して解決しようとしましたが、解決できませんでした。それを解決するのを手伝ってください。ありがとう、

Require Import Ascii.
Require Import String.

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Fixpoint ble_nat (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Definition ascii_eqb (a a': ascii) : bool :=
if ascii_dec a a' then true else false. 

(** true if s1 <= s2; s1 is before/same as s2 in alphabetical order *)
Fixpoint str_le_gt_dec (s1 s2 : String.string) 
 : bool :=
 match s1, s2 with 
 | EmptyString, EmptyString => true
 | String a b, String a' b' => 
        if ascii_eqb a a' then str_le_gt_dec b b'
        else if ble_nat (nat_of_ascii a) (nat_of_ascii a')
         then true else false
 | String a b, _ => false
 | _, String a' b' => true
 end.

Fixpoint aux (s: String.string) (ls: list String.string) 
 : list String.string :=
 match ls with 
 | nil => s :: nil
 | a :: l' => if str_le_gt_dec s a 
              then s :: a :: l' 
              else a :: (aux s l')
 end. 

Fixpoint sort (ls: list String.string) : list String.string :=
 match ls with 
 | nil => nil
 | a :: tl => aux a (sort tl)
 end. 

Notation "s1 +s+ s2" := (String.append s1 s2) (at level 60, right associativity) : string_scope.

Lemma sort_str_list_same: forall z1 z2 zm, 
 sort (z1 :: z2 :: zm) =
 sort (z2 :: z1 :: zm).
Proof with o.
 Admitted.