proposition: Lemma doubleI_E_sub A B a b: ordinalp A -> ordinalp B -> inc a A -> inc b B -> sub (doubleI_E a b) (A \times B).
proof: Proof. move => oA oB /(oltP oA) laA /(oltP oB) lbB. move => t tE. have tp:=(doubleI_E_pair tE). move: tE; rewrite - tp => /(doubleI_E_P2 (proj31_1 laA)(proj31_1 lbB)). move => [ha hb _]; apply:setXp_i. apply/(oltP oA); exact:(ole_ltT ha laA). apply/(oltP oB); exact:(ole_ltT hb lbB). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)