proposition: Lemma Cantor_aux r X f x: worder r -> fsiso_prop f r (induced_order r X) -> source f = substrate r -> glt r (Vf f x) x -> False.
proof: Proof. move => wor fsi sf lt1. have xsr := (arg2_sr (proj1 lt1)). set E := Zo (substrate r) (fun z => glt r (Vf f z) z). have ses: sub E (substrate r) by apply: Zo_S. have ne: nonempty E by exists x; apply: (Zo_i xsr). move: (worder_prop wor ses ne) =>[a /Zo_P [asr av] al]. move: asr (arg1_sr (proj1 av)); rewrite - sf => asf bsf. have bE: inc (Vf f a) E. apply: Zo_i; first by ue. by move /(fsi (Vf f a) a bsf asf): av => /iorder_gltP []. exact: (not_le_gt (proj1 wor) (al _ bE) av). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)