proposition: Theorem max_l n m : m <= n -> max n m = n.
proof: Proof. unfold max, le. rewrite compare_antisym. case compare_spec; auto. now destruct 2. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties