proposition: Lemma sub_total_suborders1 r F: order r -> sub F (substrate r) -> sub (total_suborders (induced_order r F)) (total_suborders r).
proof: Proof. move => or Fsr t /total_subordersP []; rewrite iorder_sr // => tF. rewrite (iorder_trans _ tF) => tor. by apply/total_subordersP; split => //; apply: (sub_trans tF Fsr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)