Reasoning about an imperative proto-language. Ending with a proof that insertionsort always finishes and returns a list which is sorted and it is a permutation of the input.
coqdoc

set, setandraise and some facts Things about lists to use in programming or to prove insertionsort.
coqdoc

Definition of an imperative proto-language
coqdoc

program concatenation, postcondition, finishing
coqdoc

Definition of insertionsort and proof that it sorts a list
coqdoc