proposition: Lemma set_le_ab_sab A B: C2 <=s A -> C2 <=s B -> dsum A B <=s A\times B.
proof: Proof. move => /set_le_2P [a0 [a1 [ha hb ne1]]]. move => /set_le_2P [b0 [b1 [hc hd ne2]]]. pose f z := Yo (Q z = C0) (J (P z) b0) (Yo (P z = b0) (J a1 b1) (J a0 (P z))). exists(Lf f (dsum A B) (A \times B)); saw; apply: lf_injective. rewrite /f; move => x /candu2P [px]; case; move =>[ra rb]. by Ytac0; apply:setXp_i. by rewrite rb; Ytac0; Ytac w;apply:setXp_i. move => u v /candu2P [pu pp] /candu2P [pv pp']; rewrite -{2} pu -{2} pv /f; case:pp; case pp';move => [sa ->] [sb ->]; Ytac0; Ytac0. - by move => /pr1_def ->. - by Ytac w; [ move/pr2_def | move/pr2_def=> t; case: w ]. - by Ytac w; [ move/pr2_def=> t; case: ne2 | move/pr2_def ]. - Ytac w1; Ytac w2. - by rewrite w1 w2. - by move/pr1_def => t; case: ne1. - by move/pr1_def. - by move/pr2_def ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)