proposition: Lemma rat_fusc n: natp n -> rat_iterator (fusc_quo n) = fusc_quo (csucc n).
proof: Proof. move => nN. move:fusc_pr => [Ha Hb Hc Hd]. have aux: forall k, natp k -> inc (BZ_of_nat (fusc (csucc k))) BZps. move => k kN;move: (NS_succ kN) => skN;apply/BZps_iP; split. by apply:BZ_of_natp_i; apply: NS_fusc. move /(BZ_of_nat_inj); apply: (fusc_nz' kN). case: (equal_or_not n \0c) => nz. by rewrite nz succ_zero fusc_quo_0 fusc_quo_1 rati_0. move:(cpred_pr nN nz); set m := cpred n; move => [mN mv]; rewrite mv. move:(NS_half (NS_succ mN)) => hN. case:(even_odd_dichot mN). + by move ->; rewrite succ_one fusc_quo_1 fusc_quo_2 rati_1. + move => [sa sb]. move:(NS_succ hN) => shN. rewrite /fusc_quo sa - (double_succ hN) (Hd _ hN) (Hc _ hN) (Hc _ shN). set A := fusc _; set B := fusc _. have aN: natp A by apply: NS_fusc. have bN: natp B by apply: NS_fusc. move:(BZ_of_nat_i aN)(BZ_of_nat_i bN) => az bz. have ->: BQ_of_nat (A +c B) = BQ_of_nat A +q BQ_of_nat B. by rewrite (BQsum_cZ az bz) (BZsum_cN aN bN). apply: (rati_lt1 (BZ_of_natp_i aN) (aux _ hN)). + move => [sa sb sc]. move:(NS_succ hN) => shN; move:(NS_succ shN) => sshN. rewrite /fusc_quo sa -(double_succ hN) (Hd _ hN) (Hd _ shN) (Hc _ shN). set A := fusc _; set B := fusc _; set C := fusc _. have aN: natp A by apply: NS_fusc. have bN: natp B by apply: NS_fusc. have cN: natp C by apply: NS_fusc. move:(BZ_of_nat_i aN)(BZ_of_nat_i bN) (BZ_of_nat_i cN) => az bz cz. have ->: BQ_of_nat (A +c B) = BQ_of_nat A +q BQ_of_nat B. by rewrite (BQsum_cZ az bz) (BZsum_cN aN bN). have ap: inc (BZ_of_nat A) BZp by exact (BZ_of_natp_i aN). have bp: inc (BZ_of_nat B) BZps by apply: aux. have ->: BQ_of_nat (B +c C) = BQ_of_nat B +q BQ_of_nat C. by rewrite (BQsum_cZ bz cz) (BZsum_cN bN cN). have r2N:= (NS_double (NS_rem B aN)). rewrite (proj2 (rati_gt1 ap bp)) (BZsum_cN aN bN) (BZrem_cN aN bN). rewrite - (fusc_rem hN) - (BZsum_cN cN r2N) (BZprod_cN NS2 (NS_rem B aN)). by rewrite (BZdiff_sum1 (BZ_of_nat_i r2N) cz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)