proposition: Lemma dropLast_last : forall a (l: list A), l <> nil -> dropLast (l ++ a::nil) = l.
proof: Proof. induction l; trivial. intros; simpl. destruct l; trivial. destruct ((a1 :: l) ++ a::nil). absurd (dropLast nil = a1 :: l). simpl; discr. apply IHl; discr. rewrite IHl; trivial. discr. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)