proposition: Lemma induced_wor r A: worder r -> sub A (substrate r) -> worder (induced_order r A).
proof: Proof. move=> [or wo] As; move: (iorder_osr or As) => [pa pb]. split; [exact | rewrite pb => x sx nex]. rewrite (iorder_trans _ sx). by apply: wo=>//; apply: sub_trans As. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)