proposition: Lemma worder_rc_op (p:property) : worder_rc (fun x y => [/\ p x, p y & x <=o y]).
proof: Proof. apply: worder_rc_ord. - by move => x y [_ _]. - split. + move =>x y z [pa pb pc][pd pe pf]; split => //; exact: oleT pc pf. + move =>x y [_ _ pc][ _ _ pf]; exact: oleA pc pf. + by move => x y [pa pb [pc pd _]]; split; split => //; apply: oleR. - move => x y [pa _ [pc _ _]][ pb _ [pf _ _]]. by case: (oleT_ee pc pf) => le; [left | right]; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)