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