proposition: Lemma max_l : forall x y, y<=x -> max x y = x.
proof: Proof. intros x y H. unfold max. case compare_spec; auto. intros H'. apply le_nlt in H. now elim H. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef