proposition: Lemma padd_len_lt_cons : forall (w1 w2:(list nat)), (lt (length w1) (length w2)) -> exists (w:(list nat)), (padd w1 w2)=(cons 0 w).
proof: Proof. intros. unfold padd. unfold dist. elim (minus_lt_S (length w1) (length w2) H). intros. rewrite H0. simpl. exists (app (zs x) w1). trivial. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef