proposition: Lemma the_greatest_opposite r: order r -> has_least r -> the_greatest (opp_order r) = the_least r.
proof: Proof. move=> or /(the_least_pr or) /(least_opposite or) hy. apply: the_greatest_pr2 => //; apply: (proj1 (opp_osr or)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)