proposition: Lemma fusc2_injective n m: natp n -> natp m -> fusc n = fusc m -> fusc (csucc n) = fusc (csucc m) -> n = m.
proof: Proof. wlog H: n m / n <=c m. move => Hrec nN mN sa sb. case: (NleT_ee nN mN) => h //; first by apply: Hrec. symmetry; apply: Hrec => //. move:fusc_pr => [Ha Hb Hc Hd]. move => na nb; move: m nb n na H; apply: fusc_induction. + by move => n nN /cle0. + move => n nN nle1;case: (equal_or_not n \1c) => // h. have /cle0 mz: (n <=c \0c) by apply /(cltSleP NS0); rewrite succ_zero; split. by rewrite mz Ha Hb. + move => n nN Hrec m mN le1. move: (NS_half mN)(NS_half (NS_succ nN)) => hN hnN. move: (NS_succ hN) => shN. move: (NS_fusc hN)(NS_fusc shN) (NS_fusc (NS_succ nN)) => fa fb fc. case: (cdouble_halfV mN) => em. have sb:chalf m <=c n by apply /(double_monotone hN nN); rewrite - em. rewrite em (Hc _ hN) (Hc _ nN) (Hd _ hN) (Hd _ nN). move => eq3 eq4; congr cdouble; apply: (Hrec _ hN sb eq3). by apply:(csum_eq2l fa fb fc); rewrite eq4 eq3. rewrite em - (double_succ hN) (Hc _ nN) (Hc _ shN) (Hd _ hN) (Hd _ nN). move => <-; rewrite csumC csumA -{1} (Nsum0l fb) => eq4. move:(csum_eq2r fb NS0 (NS_sum fc fa) eq4) => eq5. by move:(proj1 (csum_nz (esym eq5))) => eq6;case: (fusc_nz' nN). + move => n nN Hrec1 Hrec2 m mN le1. have hN:=(NS_half mN). rewrite - (double_succ nN) (Hd _ nN) (Hc _ (NS_succ nN)). move: (NS_fusc (NS_succ hN))(NS_fusc (NS_succ nN)) (NS_fusc nN)=> fb fc fd. case: (cdouble_halfV mN) => em. rewrite em (Hc _ hN) (Hd _ hN) => ->; rewrite csumC csumA - {2} (Nsum0l fc). move/(csum_eq2r fc (NS_sum fb fd) NS0) => /csum_nz [ha _]. by case: (fusc_nz' hN). rewrite em - (double_succ hN) (Hc _ (NS_succ hN)) (Hd _ hN). move=> eq1 eq2; rewrite eq2 in eq1. move:(csum_eq2r fc (NS_fusc hN) fd eq1) => eq3. have sb: chalf m <=c n. have wa: cardinalp (cdouble (chalf m)) by rewrite /cdouble; fprops. have wb: cardinalp (cdouble n) by rewrite /cdouble; fprops. by apply/(double_monotone hN nN); apply/(cleSSP wa wb); rewrite - em. congr (csucc (cdouble _)); apply:(Hrec1 _ hN sb eq3 eq2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)