proposition: Lemma fusc_quo_bijection: bijection_prop (Lf fusc_quo Nat BQp) Nat BQp.
proof: Proof. hnf; aw; split => //; apply: lf_bijective. + apply:QpS_fusc_quo. + move => u v uN vN eq. move: (f_equal Qnum eq)(f_equal Qden eq). move: (fusc_quo_numden uN) (fusc_quo_numden vN) => [-> ->] [-> ->]. by move /pr1_def => e1 /pr1_def e2; apply:fusc2_injective. + move => y yp. move/BQ_P: (BQp_sBQ yp) => [sa sb sc sd]. move: (BQdiv_numden (BQp_sBQ yp)) => eq0. move /Zo_P: yp =>[_ aap]. set a := P (P y); set b := P (Q y). have aN: natp a by apply:(BZ_valN sb). have bN: natp b by apply:(BZ_valN (BZps_sBZ sc)). have bv1: (BZ_of_nat b) = (Q y) by apply:(BZp_hi_pr (BZps_sBZp sc)). have bnz : b <> \0c by move => h; move:(BZps_nz sc); rewrite - bv1 h. have av1: (BZ_of_nat a) = (P y) by apply:(BZp_hi_pr). rewrite - av1 - bv1 in sd eq0. move:(fusc2_surjective aN bN bnz sd) => [n [nN na nb]];exists n => //. by rewrite /fusc_quo na nb - eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)