proposition: Lemma doubleI_E_P2 a b: ordinalp a -> ordinalp b -> forall x y, inc (J x y) (doubleI_E a b) <-> [/\ x <=o a, y <=o b & (x <> a \/ y <> b)].
proof: Proof. move => oa ob x y. apply:(iff_trans (doubleI_E_P1 oa ob x y)); split. case. - move => [-> [leyb ynb]]; split;fprops. - move => [[lexa xna] ->]; split;fprops. - move => [ [lexa xna] [leyb ynb]]; split;fprops. move => [/ole_eqVlt eq1 /ole_eqVlt eq2 eq3]. case: eq1 => xa. constructor 1; case: eq2 => yb; [by case: eq3 | done]. by case: eq2 => yb; [constructor 2 | constructor 3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)