proposition: Lemma total_order_sub r x: total_order r -> sub x (substrate r) -> total_order (induced_order r x).
proof: Proof. move=> [or tor] xs; move: (iorder_osr or xs) => [pa pb]. split; [ by exact | rewrite pb /ocomparable;aw; move=> a b asr bsr]. by case:(tor _ _ (xs _ asr) (xs _ bsr)) =>h; [left | right]; apply/iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)