proposition: Lemma fusc_rem n (A :=fusc n) (B := fusc (csucc n)) : natp n -> fusc (csucc (csucc n)) +c cdouble (A %%c B) = (A +c B).
proof: Proof. move:fusc_pr => [Ha Hb Hc Hd]; rewrite /A/B; clear A B;move: n. apply: fusc_induction. + rewrite succ_zero Ha Hb succ_one fusc2 (csum0l CS1) -(crem_small NS1 clt_01). by rewrite cdouble0 (csum0r CS1). + rewrite succ_one fusc2 fusc3 Hb csum_11 (proj33 (cdivides_one NS1)). by rewrite cdouble0 (csum0r CS2). + move => k kN _. rewrite (Hc _ kN) (Hd _ kN) - (double_succ kN) (Hc _ (NS_succ kN)). move: (NS_fusc (NS_succ kN)) (NS_fusc kN). set u := fusc _; set v := fusc _ => uN vN. have lvvu: v <c (v +c u) by apply: (csum_M0lt vN); apply: fusc_nz'. by rewrite -(crem_small (NS_sum vN uN) lvvu) csumA csum_nn csumC. + move => k kN; move: (NS_succ kN)=> sN HR1 _. rewrite - (double_succ kN) (Hc _ sN) (Hd _ sN) (Hd _ kN). move:(crem_prop (NS_fusc sN) (fusc_nz' kN) NS1 (NS_fusc kN)). rewrite (cprod1r (CS_nat (NS_fusc sN))) csumC => ->. by rewrite - csumA HR1 csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)