proposition: Lemma max_1_l n : max 1 n = n.
proof: Proof. unfold max. case compare_spec; auto. intros H. apply lt_nle in H. elim H. apply le_1_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef