proposition: Lemma min_1_l n : min 1 n = 1.
proof: Proof. unfold min. 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