proposition: Lemma fusc_quo_inv_props (F := fusc_quo_inv): [/\ (forall q, ratp q -> inc (F q) BQp), (forall x, inc x BQps -> x <> \1q -> inc (F x) BQps), (forall n, natp n -> F(fusc_quo (csucc (cdouble n))) = (fusc_quo n)) & (forall n, natp n -> n <> \0c -> F(fusc_quo (cdouble n)) = (fusc_quo n))].
proof: Proof. have Ha: forall x, \1q <=q x -> F x = (x -q \1q). by move => x sa; rewrite /F/fusc_quo_inv; Ytac0. have Hb: forall x, \0q <q x -> x <q \1q -> F x = (BQinv (BQinv x -q \1q)). move => x ha hb; rewrite /F/fusc_quo_inv; Ytac0; Ytac h => //;BQo_tac. have Hc: forall q, q <q \1q -> \0q <q q -> inc (F q) BQps. move => q qa qb; rewrite (Hb _ qb qa); apply:QpsS_inv. have qp: inc q BQps by apply / qlt0xP. apply/(qlt_diffP QS1 (QS_inv (proj31_1 qa))); rewrite -BQinv_1. by apply/(BQinv_mon2 QpsS1 qp). split. + move=> q qQ; case: (qleT_el QS1 qQ) => h. by rewrite (Ha _ h); apply/(qle_diffP QS1 qQ). case: (qleT_el qQ QS0) => h1. rewrite /F/fusc_quo_inv; Ytac ha; [ |Ytac hb; last apply:QpS0]; BQo_tac. by apply:BQps_sBQp; apply:Hc. + move => x / qlt0xP xp /nesym xnz; move: (proj32_1 xp) => xq. case: (qleT_el QS1 xq) => h; last by apply: Hc. by rewrite (Ha _ h); apply/(qlt_diffP QS1 xq). + move => n nN; move:(QpS_fusc_quo nN) => ha. rewrite(fusc_quo_odd nN) (Ha _ (BQsum_Mp QS1 ha)). by rewrite (BQdiff_sum QS1 (BQp_sBQ ha)). + move => n nN nz; rewrite(fusc_quo_even nN nz). move:(QpsS_fusc_quo nN nz) => he; move:(BQps_sBQ he)=> hf. have ha := (QpsS_inv he). have hb :=(BQsum_Mps QS1 ha). have hb' := (QpsS_sum_rl QpsS1 ha). move/ qlt0xP: (QpsS_inv hb') => hc. have hd: BQinv (\1q +q BQinv (fusc_quo n)) <q \1q. rewrite -{2} BQinv_1; apply /(BQinv_mon2 hb' QpsS1). apply:(BQsum_Mps QS1 ha). rewrite (Hb _ hc hd) (BQinv_K (proj32_1 hb)). by rewrite (BQdiff_sum QS1 (BQps_sBQ ha)) (BQinv_K hf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)