proposition: Lemma fusc_is_even n: natp n -> (evenp (fusc n) <-> n %%c \3c = \0c).
proof: Proof. move:fusc_pr => [Ha Hb Hc Hd]; move: n. move: div3_props => [pa pb pc]. apply:fusc_induction. + rewrite Ha; split;[ exact | move => _; exact: even_zero]. + rewrite Hb;split => h;first by case:(proj2 odd_one). by case: (card1_nz); rewrite - h pb. + move => k kN; rewrite (Hc _ kN) => h; apply: (iff_trans h (double_mod3 kN)). + move => k kN; rewrite (Hd _ kN); move: (NS_succ kN) => skN. have ->: csucc (cdouble k) = k +c csucc k. by rewrite (csum_nS _ kN) /cdouble - csum_nn. move: (crem_sum NS3 card3_nz kN skN); rewrite /eqmod => ->. move:(NS_fusc kN)(NS_fusc skN) => fa fb. case: (p_or_not_p (evenp (fusc k))) => eu sa sb. apply: (iff_trans (csum_of_evenP eu fb)). by move/sa:eu ->; rewrite (Nsum0l (NS_rem \3c skN)) (cmodmod3 skN). apply:(iff_trans (csum_of_oddP (conj fa eu) fb)); split; last first. move => ha; split; [ done | move/sb => hb; move: ha]. by rewrite hb (Nsum0r (NS_rem \3c kN)) (cmodmod3 kN) => /sa. move: (crem_sum NS3 card3_nz kN NS1); rewrite pb - (Nsucc_rw kN) => eq1 ev. have H3: (\2c +c \1c) %%c \3c = \0c. by rewrite -(Nsucc_rw NS2) (proj1 div3_props2). move:(div3_vals kN); case => sd. + by case: eu; apply/sa. + by move: eq1; rewrite sd /eqmod => ->; rewrite csum_11 pc csumC. + by case: (proj2 ev); apply/sb; move:eq1; rewrite sd /eqmod H3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)