proposition: Lemma fusc_quo_odd n: natp n -> fusc_quo (csucc (cdouble n)) = \1q +q (fusc_quo n).
proof: Proof. move => nN; rewrite /fusc_quo. 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 (csucc n)) <> \0q. move/(BQ_of_nat_injective); exact (fusc_nz' nN). rewrite - (double_succ nN) (fusc_even (NS_succ nN)) (fusc_odd nN). by rewrite (BQsum_div QS1 ha1 hb1 dnz) (BQprod_1l hb1) (BQsum_cN hb ha) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)