proposition: Lemma fusc_quo_even n: natp n -> n <> \0c -> fusc_quo (cdouble n) = BQinv(\1q +q BQinv (fusc_quo n)).
proof: Proof. move => nN nz; rewrite /fusc_quo. rewrite (fusc_odd nN) (fusc_even nN). move: (NS_fusc nN) (NS_fusc (NS_succ nN)) => ha hb. move:(QS_of_nat ha) (QS_of_nat hb) => ha1 hb1. have dnz: BQ_of_nat (fusc n) <> \0q. move/(BQ_of_nat_injective); exact (fusc_nz nN nz). rewrite (BQinv_div ha1 hb1) (BQsum_div QS1 hb1 ha1 dnz) (BQprod_1l ha1). by rewrite (BQinv_div (QSs ha1 hb1) ha1) (BQsum_cN ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)