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