proposition: Lemma set_le_ab_sab2 A B: A \times B <=s coarse (dsum A B).
proof: Proof. pose f x y := (J (J x C0) (J y C1)). exists (Lf (fun z => f (P z) (Q z)) (A\times B) (coarse ((dsum A B)))). saw; apply: lf_injective. move => t /setX_P [ pt qa qb]. apply:setXp_i; [ by apply: candu2_pra | by apply: candu2_prb]. move => u v /setX_P [ pu qa qb] /setX_P [ pv qc qd]. by move=> /pr12_def [ /pr1_def ha /pr1_def hb]; apply: pair_exten. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)