proposition: Theorem length_decrease: forall p x, p <> nil -> (length (fst (div p x)) < length p)%nat.
proof: Proof. intros p x; elim p; simpl; auto. intros H1; case H1; auto. intros a l; case l; simpl; auto. intros a1 l1. match goal with |- context[fst ?A] => case A end; simpl; auto with zarith. intros p1 _ H H1. apply (Nat.succ_lt_mono (length p1)); apply H; intros; discriminate. Qed.
imports: ZArith List UList Tactic Permutation