proposition: Lemma padd_cons_0 : forall (w1 w2:(list nat)) (a:nat), (length w1) = (length w2) -> (padd w1 (cons a w2)) = (cons 0 w1).
proof: Proof. intros. unfold padd. unfold dist. rewrite H. simpl length. rewrite (minus_Sn_n (length w2)). simpl. trivial. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef