proposition: Theorem max_r n m : n <= m -> max n m = m.
proof: Proof. unfold max, le. case compare; trivial. now destruct 1. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties