proposition: Lemma order_le_total a b: worder a -> worder b -> a<=O b \/ b <=O a.
proof: Proof. move => woa wob; move: (proj1 woa)(proj1 wob) => oa ob. case: (isomorphism_worder_exists woa wob) => - [f [sf is1]]. by left; apply:(order_le_alt oa ob); exists f. by right; apply:(order_le_alt ob oa); exists f. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)