proposition: Lemma least_greatest_pr r (E := substrate r): order r -> [/\ (has_least r -> forall a, inc a E -> sup r (the_least r) a = a), (has_greatest r -> forall a, inc a E -> inf r a (the_greatest r) = a), (has_least r -> forall a, inc a E -> inf r (the_least r) a = (the_least r))& (has_greatest r -> forall a, inc a E -> sup r a (the_greatest r) = (the_greatest r))].
proof: Proof. move=> or; split. + move => h a asr; apply: sup_comparable1 => //. by move: (the_least_pr or h) => [_ sp]; apply: sp. + move => h a asr; apply: inf_comparable1 => //. by move: (the_greatest_pr or h) => [_ sp]; apply: sp. + move => h a asr; apply: inf_comparable1 => //. by move: (the_least_pr or h) => [_ sp]; apply: sp. + move => h a asr; apply: sup_comparable1 => //. by move: (the_greatest_pr or h) => [_ sp]; apply: sp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)