proposition: Lemma finite_subset_torder_greatest r X: total_order r -> finite_set X -> nonempty X -> sub X (substrate r) -> has_greatest (induced_order r X).
proof: Proof. move=> [or tor]. move: X;apply: finite_set_induction3. + move=> a b asr bsr. have sd: sub (doubleton a b) (substrate r) by apply: sub_set2. have aux: (substrate (induced_order r (doubleton a b))) = doubleton a b. by rewrite iorder_sr. by case: (tor _ _ asr bsr)=> cp; [exists b | exists a]; hnf;rewrite aux; split; fprops; move=> x /set2_P [] ->; apply/iorder_gle0P; fprops; order_tac. + move=> a b x y asr bsr;rewrite /greatest. have sta: (sub (a +s1 b) (substrate r)) by apply: setU1_sub. rewrite iorder_sr //; move=> [xa xp]. have xsr := (asr _ xa). have sd: sub (doubleton x b) (substrate r) by apply: sub_set2. move: xp; rewrite iorder_sr //; move=> xp [yd yp]. rewrite iorder_sr //;split. move: yd => /set2_P []->; fprops. have xy:= (iorder_gle1 (yp _ (set2_1 x b))). have lby:= (iorder_gle1 (yp _ (set2_2 x b))). have yt: inc y (a +s1 b) by case /set2_P: yd => ->; fprops. move=> z zi; apply /iorder_gle0P => //. case /setU1_P: zi => h; last by ue. have zx:=(iorder_gle1 (xp _ h)) ; order_tac. + move=> Z x Zs neZ [h gex]; apply: (Zs). by move: h; rewrite iorder_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)