proposition: Lemma lattice_opposite r: lattice r -> lattice (opp_order r).
proof: Proof. move=> [or lr]; move: (opp_osr or) => [oor soi]; split => //. rewrite soi; move=> x y xs ys. have [[x1 p1] [x2 p2]] := (lr _ _ xs ys). split. by exists x2; apply /(inf_sup_oppP or) => //; apply: sub_set2. by exists x1; apply /(sup_inf_oppP or) => //; apply: sub_set2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)