proposition: Lemma sub_total_suborders2 r X Y: order r -> inc X (total_suborders r) -> sub Y X -> inc Y (total_suborders r).
proof: Proof. move =>or /total_subordersP [ha hb] hc; apply/total_subordersP. have s1 : sub Y (substrate (induced_order r X)) by rewrite iorder_sr//. move: (sub_trans hc ha) => s2. by move: (total_order_sub hb s1); rewrite (iorder_trans _ hc) => tor. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)