proposition: Lemma wlt_gt_length : forall (w1 w2:(list nat)), (wlt w1 w2) -> (lt (length w2) (length w1)) -> exists (n:nat) (w:(list nat)), (w1 = (app (zs n) w)) /\ (length w)=(length w2) /\ (wlt w w2).
proof: Proof. induction w1 as [| a w1 IHw1]; [intros w2 _ []%Nat.nlt_0_r |]. intros w2 H Hl; simpl in Hl; apply <-Nat.succ_le_mono in Hl. destruct a as [| a]. - apply Nat.le_lteq in Hl as [Hl | Hl]. + apply wlt_0_w_inv in H; specialize (IHw1 w2 H Hl) as [n [w' [H'1 [H'2 H'3]]]]. now exists (S n); exists w'; split; [rewrite H'1 | split]. + exists (S 0); exists w1; split; [reflexivity | split]; [now symmetry |]. exact (wlt_0_w_inv _ _ H). - now exfalso; apply not_wlt_len_left with (2 := H). Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef