This is a Coq formalisation of various sorting algorithms, using the sauto tactic from CoqHammer.
sauto
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.