proposition: Lemma min_idempotent : forall a, min a a a.
proof: Proof. intros. constructor. - reflexivity. - reflexivity. - intros. assumption. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat