proposition: Lemma aleph_of_prop2 a b: aleph_of a b -> (a <=s (substrate b) \/ (substrate b) <=s a) -> exists2 r, worder_on r a & b \Is r.
proof: Proof. move => [ha / set_lt_notP hb / set_lt_notP hc] hd. have /EqS [f fp]: a \Eq (substrate b). case: hd; move => [f fp]; [ apply: (hc f fp) | apply: EqS; apply:(hb f fp)]. exact:(worder_transportation (conj ha (erefl (substrate b))) fp). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)