-
Guillaume Melquiond authored
From Max_is_some and Max_is_ge, one can prove that ge is a total relation. So the consequents hold even if "ge x y" does not (since "ge y x" then holds by totality).
7b2226a8
From Max_is_some and Max_is_ge, one can prove that ge is a total relation. So the consequents hold even if "ge x y" does not (since "ge y x" then holds by totality).