proposition: Lemma the_least_opposite r: order r -> has_greatest r -> the_least (opp_order r) = the_greatest r.
proof: Proof. move=> or /(the_greatest_pr or) /(greatest_opposite or) hy. apply: the_least_pr2 => //; apply: (proj1 (opp_osr or)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)