proposition: Lemma Eq_sum_mono2 A B C: A <=s B -> (dsum A C) <=s (dsum B C).
proof: Proof. move =>[f [[ff fi] sf tb]]. exists (Lf (fun p=> Yo (Q p = C0) (J (Vf f (P p)) C0) p) (dsum A C) (dsum B C)). saw; apply:lf_injective. move => t /candu2P [pt]; case => - [qa qb];rewrite qb; Ytac0. apply: candu2_pra; Wtac. by rewrite -pt qb;apply: candu2_prb. move: C0_ne_C1 C1_ne_C0 => pa pb. move => u v /candu2P [pu ha] /candu2P [pv hb];case: ha; case: hb. - rewrite -{6} pv - {6} pu ;move =>[sa ->] [sb ->]; Ytac0; Ytac0 => /pr1_def h. congr J; apply: fi => //;ue. - rewrite -{5} pv; move =>[sa ->] [sb ->]. by Ytac0; Ytac0 => /pr2_def h; case:pa. - rewrite -{5} pu; move =>[sa ->] [sb ->]. by Ytac0; Ytac0 => /pr2_def h; case:pa. - by move =>[sa ->] [sb ->] ; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)