proposition: Lemma BQ_moebius_props2 x (f := fun z=> \1q /q (\1q -q z)) (g := fun z => \1q -q (\1q /q z)): ratp x -> ((x <> \1q -> g (f x) = x) /\ (x <> \0q -> f (g x) = x)).
proof: Proof. move => xq. have pa: ratp (\1q -q x) by apply:(QS_diff QS1 xq). have pb: forall x, ratp x -> \1q /q x = BQinv x. by move => y yq; rewrite /BQdiv BQprod_1l //; apply:QS_inv. split => xn1; rewrite /f/g. have hb: \1q -q x <> \0q. move => h; move: (f_equal (fun z => x +q z) h). rewrite (BQsum_diff xq QS1) BQsum_0r; fprops. have hc:=(QS_diff QS1 xq). have hd:=(QS_inv hc). rewrite (pb _ hc) (pb _ hd) (BQinv_K hc);apply:(BQdiff_diff_simp QS1 xq). have pc:= (QS_div QS1 xq). by rewrite (BQdiff_diff_simp QS1 pc) (pb _ pc) (pb _ xq) (BQinv_K xq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)