proposition: Lemma max_r : forall x y, x<=y -> max x y = y.
proof: Proof. unfold le, max. intros x y. destruct compare; easy'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef