proposition: Lemma sumpow2_inj n K1 K2 : natp n -> (forall i, inc i K1 -> i<c n) -> (forall i, inc i K2 -> i<c n) -> sumpow2 K1 = sumpow2 K2 -> K1 = K2.
proof: Proof. pose p K n := (forall i, inc i K -> i <c n). have bd: forall n, natp n -> forall K, p K n -> sumpow2 K <c \2c ^c n. apply: Nat_induction. move => K h; rewrite cpowx0. case:(emptyset_dichot K). by move => ->; rewrite /sumpow2 /csumb csum_trivial; fprops; aw. by move => [i /h /clt0]. move => m mN Hrec K kP. set K':= K -s1 m. have /Hrec r1:(p K' m). by move => i /setC1_P [/kP /(cltSleP mN) h1 h2]. rewrite (cpow_succ _ mN) cprodC - csum_nn. case: (inc_or_not m K) => ink. rewrite (sumpow2_rec ink); apply:csum_Mlteq; fprops. rewrite -(setC1_eq ink); apply: (clt_leT r1); apply:csum_M0le; fprops. move => nN; move: n nN K1 K2; apply: Nat_induction. move => K1 K2 h1 h2 sv. case:(emptyset_dichot K1) => ha. case:(emptyset_dichot K2) => hb; first by rewrite ha hb. by move:hb => [i/h2 /clt0]. by move:ha => [i/h1 /clt0]. move => n nN Hrec K1 K2 h1 h2. have kk1:(p (K1 -s1 n) n). by move => i /setC1_P [/h1 /(cltSleP nN) hu hv]. have kk2:(p (K2 -s1 n) n). by move => i /setC1_P [/h2 /(cltSleP nN) hu hv]. have l1:= bd _ nN _ kk1. have l2:= bd _ nN _ kk2. have pN:= (NS_pow NS2 nN). case: (inc_or_not n K1) => nk1; case: (inc_or_not n K2) => nk2. + have hh1:= (NS_lt_nat l1 (NS_pow NS2 nN)). have hh2:= (NS_lt_nat l2 (NS_pow NS2 nN)). rewrite (sumpow2_rec nk1) (sumpow2_rec nk2) => eq2. move:(csum_eq2r pN hh1 hh2 eq2) => eq3. by rewrite - (setC1_K nk1) - (setC1_K nk2) (Hrec _ _ kk1 kk2 eq3). + move: l2; rewrite (sumpow2_rec nk1) (setC1_eq nk2) => l2 eq. move: (csum_M0le (sumpow2 (K1 -s1 n)) (CS_nat pN)). by rewrite csumC eq => /(cltNge l2). + move: l1; rewrite (setC1_eq nk1) (sumpow2_rec nk2) => l1 eq. move: (csum_M0le (sumpow2 (K2 -s1 n)) (CS_nat pN)). by rewrite csumC - eq => /(cltNge l1). + by rewrite - (setC1_eq nk1) - (setC1_eq nk2); apply: Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)