proposition: Lemma Exercise4_8j K (o := opp_order (induced_order r K)) (A:= increasing_mappings o E48Io) (no := increasing_mappings_order o E48Io): sub K (substrate r) ->order_on no A.
proof: Proof. move=> Ksr; move: (Exercise4_8f Ksr) Exercise4_8h => [p1 p2] [p3 p4]. by apply: imo_osr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)