demazure This project contains formalizations of some facts about almost-sign-preserving permutations and the Demazure product on them.