proposition: Theorem cle_wor: worder_r cardinal_le.
proof: Proof. split => //. split => //. - move=> a b c;apply: cleT. - move=> a b; apply: cleA. - move=> x y [cx cy _]; split; fprops. move=> x xa xne. have xc: cardinal_set x by move=> b bx; move: (xa _ bx)=> [ok _]. have [ip ii]:=(cle_wor' xc xne); exists (intersection x). hnf; rewrite (graph_on_sr xa); split => //. by move=> u ux;move: (ii _ ux) => uy; apply graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)