proposition: Lemma min_idempotent : forall a, eq (min a a) a.
proof: Proof. intros. apply PO.min_unique with a a. apply min_ok. apply PreO.min_idempotent. apply PO.PreO. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat