proposition: Lemma min_assoc : forall a b c, eq (min a (min b c)) (min (min a b) c).
proof: Proof. intros. apply PO.min_unique with a (min b c). - apply min_ok. - apply <- (PreO.min_assoc _ a b c); apply min_ok. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat