Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]