-
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
Prochaines maintenances programmées: mardi 02/04, lundi 06/05, lundi 03/06
Pour plus d'informations: https://doc-si.inria.fr/display/SU/Gitlab
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).