proposition: Lemma max_l n m : m<=n -> max n m = n.
proof: Proof. unfold le, max. rewrite (compare_antisym n m). case compare; intuition. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass