proposition: Lemma doubleI_E_P1 a b: ordinalp a -> ordinalp b -> forall x y, inc (J x y) (doubleI_E a b) <-> [\/ x = a /\ y <o b, x <o a /\ y = b | x <o a /\ y <o b].
proof: Proof. move => oa ob x y; split. case/setU2_P; first case/setU2_P. - by move/setXp_P => [/set1_P -> /(oltP ob) lyb]; constructor 1. - by move/setXp_P => [/(oltP oa) lxa /set1_P -> ]; constructor 2. - by move/setXp_P => [/(oltP oa) lxa /(oltP ob) lyb ]; constructor 3. case => - [pa pb]; apply/setU2_P. - rewrite pa;left; apply/setU2_P; left; apply:setXp_i; fprops. by apply/(oltP ob). - rewrite pb;left; apply/setU2_P; right; apply:setXp_i; fprops. by apply/(oltP oa). - by right; apply:setXp_i; [ apply/(oltP oa) | apply/(oltP ob) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)