proposition: Lemma finite_set_minimal r: order r -> finite_set (substrate r) -> nonempty (substrate r) -> exists x, minimal r x.
proof: Proof. move => or. move: (opp_osr or) => [or' sr']. rewrite - sr' => fsr nes. move: (finite_set_maximal or' fsr nes) => [x xf]; exists x. by apply /maximal_opp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)