proposition: Lemma BQ_moebius_props1 x (f := fun z=> z /q (\1q +q z)) (g := fun z => z /q (\1q -q z)): ratp x -> ((x <> \1mq -> g (f x) = x) /\ (x <> \1q -> f (g x) = x)).
proof: Proof. move => xq. have pa: inc (\1q +q x) BQ by apply:(QSs QS1 xq). split => xn1; rewrite /f/g. have qa: \1q +q x <> \0q. move => h; move: (f_equal (fun z => z +q \1mq) h). rewrite (BQsumC \1q) - (BQsumA xq QS1 QSm1) - {1} BQopp_1. by rewrite -/(_ -q _) (BQdiff_xx QS1) (BQsum_0r xq) (BQsum_0l QSm1). rewrite (BQdiff_div QS1 xq pa qa) (BQprod_1l pa). rewrite {2} (BQsumC \1q) (BQdiff_sum xq QS1). by rewrite (BQdiv_div_simp xq pa QS1 qa) BQdiv_x1. have ha:= (QS_diff QS1 xq). have hb: \1q -q x <> \0q. move /(f_equal (fun z => x +q z)). rewrite (BQsum_diff xq QS1) (BQsum_0r xq); fprops. rewrite (BQsum_div QS1 xq ha hb) (BQprod_1l ha)(BQsumC _ x). by rewrite (BQsum_diff xq QS1) (BQdiv_div_simp xq ha QS1 hb) BQdiv_x1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)