proposition: Lemma worder_total r: worder r -> total_order r.
proof: Proof. move=> wor; move: (proj1 wor) => or; split=> // x y xs ys. move:(set2_1 x y)(set2_2 x y);set (u:=doubleton x y) => xu yu. have ur: sub u (substrate r) by apply: sub_set2. have si: substrate (induced_order r u) = u by rewrite iorder_sr. have neu: nonempty u by ex_tac. move: (worder_prop wor ur neu)=> [z zu zle]. move: (zle _ xu)(zle _ yu) => p1 p2. by case /set2_P: zu => <-; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)