proposition: Lemma padd_len_le_len : forall (w1 w2:(list nat)), (le (length w1) (length w2)) -> (length (padd w1 w2)) = (length w2).
proof: Proof. intros. unfold padd. unfold dist. rewrite app_length. rewrite zs_len. rewrite Nat.sub_add by (exact H); reflexivity. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef