proposition: Theorem list_last_cons_app : ∀ A x y (l : list A) d, List.last [x … l ++ [y]] d = y.
proof: Proof. intros A x y l d. revert x. induction l as [| z]; [ reflexivity | intros ]. simpl in IHl; simpl. apply IHl. Qed.
imports: Utf8 QArith NPeano Sorted Psatz