proposition: Lemma Eq_sum_mono1 A B: A <=s (dsum A B).
proof: Proof. exists (Lf (fun z => J z C0) A (dsum A B)). saw;apply: lf_injective; first apply:candu2_pra. by move => u v _ _ /pr1_def. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)