proposition: Lemma set_le_total r A s B: worder_on r A -> worder_on s B -> A <s B \/ B <=s A.
proof: Proof. move =>[wor1 sr1][wor2 sr2]. have aux u v: u <=O v -> set_le (substrate u) (substrate v). move => [_ ov [f [x [xs [_ _ bp _]]]]]. move: bp; rewrite (iorder_sr ov xs) => bp. by apply/set_leP; exists x => //; exists f. case: (order_le_total wor1 wor2); move/aux; rewrite sr1 sr2;last by right. move => lee. case: (p_or_not_p (A \Eq B)) => h; last by left. by right; apply/set_leP; exists A => //; apply: EqS. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)