proposition: Lemma min_glb : forall x y z, z <= x -> z <= y -> z <= min x y.
proof: Proof. intros. destruct (le_total x y). rewrite -> min_def1; assumption. rewrite -> min_def2; assumption. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice